[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
# .	charlist	f	charset → nat
# .	string-less	f	string → nat
# .	charlist	f	charlist → nat
#oc	charlist	f	char × charlist → nat
. '	string-append	f	char → string
. '	charlist	f	char → charlist
. + .	string-data	f	char × string → string
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	charlist	f	char × char → charlist
. + .	charlist	f	char × charlist → charlist
. + .	charlist	f	charlist × char → charlist
. + .	charlist	f	charlist × charlist → charlist
. ++ .	charlist	f	charset × char → charset
. ++ .	charlist	f	charlist × char → charlist
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	charlist	f	charset × char → charset
. -1	nat-basic1	f	nat → nat
. -1l .	charlist	f	charlist × nat → charlist
. -l .	charlist	f	charlist × char → charlist
. -pos .	charlist	f	charlist × char → charlist
. .butlast	charlist	f	charlist → charlist
. .butmax	charlist	f	charset → charset
. .butmin	charlist	f	charset → charset
. .char1	string-data	f	string → char
. .first	charlist	f	charlist → char
. .last	charlist	f	charlist → char
. .max	charlist	f	charset → char
. .min	charlist	f	charset → char
. .rest	charlist	f	charlist → charlist
. .rstring	string-data	f	string → string
. < .	charlist	p	charset × char
. < .	charlist	p	char × charset
. < .	charlist	p	charlist × charlist
. < .	nat-basic1	p	nat × nat
. < .	string-less	p	char × char
. < .	string-less	p	string × string
. > .	nat	p	nat × nat
. [ . ]	charlist	f	charlist × nat → char
. [ . ]	charlist	f	charlist × nat × char → charlist
. \ .	charlist	f	charlist × charlist → charlist
. \ .	charlist	f	charset × charset → charset
. ∈ .	charlist	p	char × charset
. ∈ .	charlist	p	char × charlist
. ∩ .	charlist	f	charset × charset → charset
. ∪ .	charlist	f	charlist × charlist → charlist
. ∪ .	charlist	f	charset × charset → charset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	charlist	p	charset × charset
. ⊆ .	charlist	p	charlist × charlist
. ⊆m .	charlist	p	charlist × charlist
. ⊑ .	charlist	p	charlist × charlist
. ⊒ .	charlist	p	charlist × charlist
[]	charlist	c	charlist
{ . }	charlist	f	char → charset
∅	charlist	c	charset
butlastn	charlist	f	nat × charlist → charlist
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
charlist	charlist	s
chars	charlist	v	charlist
chars0	charlist	v	charlist
chars1	charlist	v	charlist
chars10	charlist	v	charlist
chars2	charlist	v	charlist
chars3	charlist	v	charlist
chars4	charlist	v	charlist
chars5	charlist	v	charlist
chars6	charlist	v	charlist
chars7	charlist	v	charlist
chars8	charlist	v	charlist
chars9	charlist	v	charlist
charset	charlist	s
charset	charlist	v	charset
charset0	charlist	v	charset
charset1	charlist	v	charset
charset2	charlist	v	charset
disj	charlist	p	charlist × charlist
dups	charlist	p	charlist
fillfirst	charlist	f	nat × char × charlist → charlist
filter	charlist	f	charlist × charlist → charlist
firstn	charlist	f	nat × charlist → charlist
frome	charlist	f	charlist × char → charlist
ins≤	charlist	f	char × charlist → charlist
l→s	string2list	f	charlist → string
lastn	charlist	f	nat × charlist → charlist
list2set	charlist	f	charlist → charset
m	nat-basic1	v	nat
merge	charlist	f	charlist × charlist → charlist
mklist	charlist	f	char × nat → charlist
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
ordered<	charlist	p	charlist
ordered≤	charlist	p	charlist
perm	charlist	p	charlist × charlist
pos	string-less	f	char × string → nat
pos	charlist	f	char × charlist → nat
restn	charlist	f	nat × charlist → charlist
rev	charlist	f	charlist → charlist
rmdup	charlist	f	charlist → charlist
s→l	string2list	f	string → charlist
set2list	charlist	f	charset → charlist
sortedchars	string-less	c	string
str	string-data	v	string
str0	string-data	v	string
str1	string-data	v	string
str2	string-data	v	string
str3	string-data	v	string
string	string-data	s
stringvar	string-append	v	string
stringvar0	string-append	v	string
sublist	charlist	f	nat × nat × charlist → charlist