[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
# .	intlista	f	intlist → nat
#oc	intlista	f	int × intlist → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	intlista	f	int → intlist
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	intlista	f	intlist × int → intlist
. + .	intlista	f	int × intlist → intlist
. + .	intlista	f	intlist × intlist → intlist
. ++ .	intlista	f	intlist × int → intlist
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. +l .	intlista	f	int × int → intlist
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. -1l .	intlista	f	intlist × nat → intlist
. -1l .	intlista	f	intlist × int → intlist
. -l .	intlista	f	intlist × int → intlist
. .butlast	intlista	f	intlist → intlist
. .first	intlista	f	intlist → int
. .last	intlista	f	intlist → int
. .rest	intlista	f	intlist → intlist
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	intlista	p	intlist × intlist
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. [ . ]	intlista	f	intlist × nat → int
. [ . ]	intlista	f	intlist × nat × int → intlist
. \ .	intlista	f	intlist × intlist → intlist
. ∈ .	intlista	p	int × intlist
. ∪ .	intlista	f	intlist × intlist → intlist
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ⊆ .	intlista	p	intlist × intlist
. ⊆m .	intlista	p	intlist × intlist
. ⊑ .	intlista	p	intlist × intlist
. ⊒ .	intlista	p	intlist × intlist
[]	intlista	c	intlist
~ .	int-abs	f	int → int
abs	int-abs	f	int → int
butlastn	intlista	f	nat × intlist → intlist
disj	intlista	p	intlist × intlist
dups	intlista	p	intlist
even	int-min	p	int
fillfirst	intlista	f	nat × int × intlist → intlist
filter	intlista	f	intlist × intlist → intlist
firstn	intlista	f	nat × intlist → intlist
frome	intlista	f	intlist × int → intlist
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
i1	intlista	v	int
i2	intlista	v	int
ins≤	intlista	f	int × intlist → intlist
int	int-basic1	s
intlist	intlista	s
ints	intlista	v	intlist
ints0	intlista	v	intlist
ints1	intlista	v	intlist
ints10	intlista	v	intlist
ints2	intlista	v	intlist
ints3	intlista	v	intlist
ints4	intlista	v	intlist
ints5	intlista	v	intlist
ints6	intlista	v	intlist
ints7	intlista	v	intlist
ints8	intlista	v	intlist
ints9	intlista	v	intlist
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	intlista	f	nat × intlist → intlist
m	nat-basic1	v	nat
max	int-min	f	int × int → int
merge	intlista	f	intlist × intlist → intlist
min	int-min	f	int × int → int
mklist	intlista	f	int × nat → intlist
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
odd	int-min	p	int
ordered<	intlista	p	intlist
ordered≤	intlista	p	intlist
perm	intlista	p	intlist × intlist
pos	intlista	f	int × intlist → nat
restn	intlista	f	nat × intlist → intlist
rev	intlista	f	intlist → intlist
rmdup	intlista	f	intlist → intlist
sgn	int-min	f	int → int
sort	intlista	f	intlist → intlist
sublist	intlista	f	nat × nat × intlist → intlist