[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
# .	natlist	f	natlist → nat
#oc	natlist	f	nat × natlist → nat
. '	natlist	f	nat → natlist
. + .	nat-basic	f	nat × nat → nat
. + .	natlist	f	nat × natlist → natlist
. + .	natlist	f	natlist × natlist → natlist
. + .	natlist	f	natlist × nat → natlist
. ++ .	natlist	f	natlist × nat → natlist
. +1	nat-basic	f	nat → nat
. +2 .	natlist	f	nat × nat → natlist
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	natlist	f	natlist × nat → natlist
. -l .	natlist	f	natlist × nat → natlist
. -p .	natlist	f	natlist × nat → natlist
. .butlast	natlist	pf	natlist → natlist with λ x. x ≠ []
. .head	natlist	pf	natlist → nat with λ x. x ≠ []
. .last	natlist	pf	natlist → nat with λ x. x ≠ []
. .tail	natlist	pf	natlist → natlist with λ x. x ≠ []
. < .	nat-basic	p	nat × nat
. < .	natlist	p	natlist × natlist
. > .	nat	p	nat × nat
. [ . ]	natlist	pf	natlist × nat → nat with λ x, n. n < # x
. [ . ]	natlist	pf	natlist × nat × nat → natlist with λ x, n, a. n < # x
. \ .	natlist	f	natlist × natlist → natlist
. ∈ .	natlist	p	nat × natlist
. ∪ .	natlist	f	natlist × natlist → natlist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	natlist	p	natlist × natlist
. ⊆m .	natlist	p	natlist × natlist
. ⊑ .	natlist	p	natlist × natlist
. ⊒ .	natlist	p	natlist × natlist
[]	natlist	c	natlist
butlastn	natlist	pf	nat × natlist → natlist with λ n, x. n ≤ # x
disj	natlist	p	natlist × natlist
dups	natlist	p	natlist
fillfirst	natlist	f	nat × nat × natlist → natlist
filter	natlist	f	natlist × natlist → natlist
firstn	natlist	pf	nat × natlist → natlist with λ n, x. n ≤ # x
frome	natlist	f	natlist × nat → natlist
ins≤	natlist	f	nat × natlist → natlist
lastn	natlist	pf	nat × natlist → natlist with λ n, x. n ≤ # x
merge	natlist	f	natlist × natlist → natlist
mklist	natlist	f	nat × nat → natlist
nat	nat-basic	s
natlist	natlist	s
ordered<	natlist	p	natlist
ordered≤	natlist	p	natlist
perm	natlist	p	natlist × natlist
pos	natlist	f	nat × natlist → nat
restn	natlist	pf	nat × natlist → natlist with λ n, x. n ≤ # x
rev	natlist	f	natlist → natlist
rmdup	natlist	f	natlist → natlist
sublist	natlist	pf	nat × nat × natlist → natlist with λ n, m, x. n + m ≤ # x