[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	list-data	f	list → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	intlist	f	int → list
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	intlist	f	int × int → list
. + .	int-basic2	f	int × int → int
. + .	intlist	f	list × int → list
. + .	nat-basic2	f	nat × nat → nat
. + .	list	f	list × list → list
. + .	intlist	f	int × list → list
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. - .	int-abs	f	int × int → int
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. .t	treeorfail	f	treeorfail → tree
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	list-data	p	list × list
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ∈ .	intlist	p	int × list
[]	list-data	c	list
~ .	int-abs	f	int → int
abs	int-abs	f	int → int
d	intlist	v	int
depths	build-base	f	tree × int → list
even	int-min	p	int
fail	treeorfail	c	treeorfail
h	intlist	v	int
head	intlist	f	list → int
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
int	int-basic1	s
is_empty	build-base	p	list
j	int-basic1	v	int
j0	int-basic1	v	int
l	tree	f	tree → tree
Leaf	tree	c	tree
list	list-data	s
m	nat-basic2	v	nat
max	int-min	f	int × int → int
max	build-base	f	list → int
min	int-min	f	int × int → int
min	build-base	f	list → int
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
Node	tree	f	tree × tree → tree
odd	int-min	p	int
pop	intlist	f	list → list
r	tree	f	tree → tree
sgn	int-min	f	int → int
some	treeorfail	f	tree → treeorfail
t	tree	v	tree
t0	tree	v	tree
t1	tree	v	tree
t2	tree	v	tree
to	treeorfail	v	treeorfail
to0	treeorfail	v	treeorfail
to1	treeorfail	v	treeorfail
tree	tree	s
treeorfail	treeorfail	s
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list