[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
# .	reflist	f	Reflist → Nat
. '	reflist	f	Ref → Reflist
. + .	nat-basic	f	Nat × Nat → Nat
. + .	reflist	f	Ref × Reflist → Reflist
. + .	reflist	f	Reflist × Reflist → Reflist
. + .	reflist	f	Reflist × Ref → Reflist
. ++ .	reflist	f	Reflist × Ref → Reflist
. +1	nat-basic	f	Nat → Nat
. +2 .	reflist	f	Ref × Ref → Reflist
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	reflist	f	Reflist × Ref → Reflist
. -l .	reflist	f	Reflist × Ref → Reflist
. -p .	reflist	f	Reflist × Nat → Reflist
. .butlast	reflist	pf	Reflist → Reflist with λ x. x ≠ []
. .last	reflist	pf	Reflist → Ref with λ x. x ≠ []
. < .	nat-basic	p	Nat × Nat
. < .	reflist	p	Reflist × Reflist
. > .	nat	p	Nat × Nat
. [ . ]	reflist	pf	Reflist × Nat → Ref with λ x, n. n < # x
. [ . ]	reflist	pf	Reflist × Nat × Ref → Reflist with λ x, n, a. n < # x
. \ .	reflist	f	Reflist × Reflist → Reflist
. ∈ .	reflist	p	Ref × Reflist
. ∪ .	reflist	f	Reflist × Reflist → Reflist
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	reflist	p	Reflist × Reflist
. ⊑ .	reflist	p	Reflist × Reflist
. ⊒ .	reflist	p	Reflist × Reflist
[]	reflist	c	Reflist
Nat	nat-basic	s
Ref	Ref	s
Reflist	reflist	s
butlastn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
disj	reflist	p	Reflist × Reflist
dups	reflist	p	Reflist
fillfirst	reflist	f	Nat × Ref × Reflist → Reflist
filter	reflist	f	Reflist × Reflist → Reflist
firstn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
frome	reflist	f	Reflist × Ref → Reflist
hd .	reflist	pf	Reflist → Ref with λ x. x ≠ []
lastn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
mklist	reflist	f	Ref × Nat → Reflist
null	Ref	c	Ref
pos	reflist	f	Ref × Reflist → Nat
restn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
rev	reflist	f	Reflist → Reflist
rmdup	reflist	f	Reflist → Reflist
sublist	reflist	pf	Nat × Nat × Reflist → Reflist with λ n, m, x. n + m ≤ # x
tl .	reflist	pf	Reflist → Reflist with λ x. x ≠ []