[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
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. \| .	int-gcd	p	int × int
. ∈ .	intlista	p	int × intlist
. ∪ .	intlista	f	intlist × intlist → intlist
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ⊆ .	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
Π .	intlist	f	intlist → int
Σ .	intlist	f	intlist → int
abs	int-abs	f	int → int
all_prime_divisors	intlist	f	int → intlist
butlastn	intlista	f	nat × intlist → intlist
coprimes	intlist	f	int → intlist
count-i2j	intlist	f	int × int → intlist
countFun	intlist	f	int × int × (int → int) → intlist
disj	intlista	p	intlist × intlist
dups	intlista	p	intlist
euler-phi	intlist	f	int → int
even	int-min	p	int
fillfirst	intlista	f	nat × int × intlist → intlist
filter	intlista	f	intlist × intlist → intlist
filterFun	intlist	f	(int → bool) × intlist → intlist
firstn	intlista	f	nat × intlist → intlist
frome	intlista	f	intlist × int → intlist
gcd	int-gcd	f	int × int → int
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
intboolfun	intlist	v	int → bool
intfun	intlist	v	int → int
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
isSquare	int-square	p	int
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	intlista	f	nat × intlist → intlist
m	nat-basic1	v	nat
mapFun	intlist	f	(int → int) × intlist → intlist
max	int-min	f	int × int → int
max	intlist	f	intlist → int
max_prime_divisor	int-gcd	f	int → int
merge	intlista	f	intlist × intlist → intlist
min	intlist	f	intlist → int
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
prime	int-gcd	p	int
primes	intlist	p	intlist
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
sqrt	int-square	f	int → int
sublist	intlista	f	nat × nat × intlist → intlist