[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
# .	string-less	f	string → nat
# .	stringlist	f	stringlist → nat
# .	charlist	f	charlist → nat
# .	charlist	f	charset → nat
#oc	stringlist	f	string × stringlist → nat
#oc	charlist	f	char × charlist → nat
. % .	nat-div	f	nat × nat → nat
. '	string-append	f	char → string
. '	stringlist	f	string → stringlist
. '	charlist	f	char → charlist
. * .	nat-mult	f	nat × nat → nat
. + .	string-data	f	char × string → string
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	stringlist	f	stringlist × string → stringlist
. + .	charlist	f	char × charlist → charlist
. + .	stringlist	f	stringlist × stringlist → stringlist
. + .	charlist	f	charlist × charlist → charlist
. + .	stringlist	f	string × stringlist → stringlist
. + .	charlist	f	charlist × char → charlist
. + .	charlist	f	char × char → charlist
. ++ .	stringlist	f	stringlist × string → stringlist
. ++ .	charlist	f	charlist × char → charlist
. ++ .	charlist	f	charset × char → charset
. +1	nat-basic1	f	nat → nat
. +l .	stringlist	f	string × string → stringlist
. - .	nat	f	nat × nat → nat
. -- .	charlist	f	charset × char → charset
. -1	nat-basic1	f	nat → nat
. -1l .	stringlist	f	stringlist × nat → stringlist
. -1l .	stringlist	f	stringlist × string → stringlist
. -1l .	charlist	f	charlist × nat → charlist
. -l .	charlist	f	charlist × char → charlist
. -l .	stringlist	f	stringlist × string → stringlist
. -pos .	charlist	f	charlist × char → charlist
. .butlast	string-ops	f	string → string
. .butlast	charlist	f	charlist → charlist
. .butlast	stringlist	f	stringlist → stringlist
. .butmax	charlist	f	charset → charset
. .butmin	charlist	f	charset → charset
. .char1	string-data	f	string → char
. .first	charlist	f	charlist → char
. .first	stringlist	f	stringlist → string
. .last	string-ops	f	string → char
. .last	stringlist	f	stringlist → string
. .last	charlist	f	charlist → char
. .max	charlist	f	charset → char
. .min	charlist	f	charset → char
. .rest	charlist	f	charlist → charlist
. .rest	stringlist	f	stringlist → stringlist
. .rstring	string-data	f	string → string
. / .	nat-div	f	nat × nat → nat
. < .	stringlist	p	stringlist × stringlist
. < .	charlist	p	charset × char
. < .	nat-basic1	p	nat × nat
. < .	charlist	p	char × charset
. < .	charlist	p	charlist × charlist
. < .	string-less	p	string × string
. < .	string-less	p	char × char
. > .	nat	p	nat × nat
. [ . ]	charlist	f	charlist × nat → char
. [ . ]	charlist	f	charlist × nat × char → charlist
. [ . ]	stringlist	f	stringlist × nat × string → stringlist
. [ . ]	stringlist	f	stringlist × nat → string
. \ .	stringlist	f	stringlist × stringlist → stringlist
. \ .	charlist	f	charlist × charlist → charlist
. \ .	charlist	f	charset × charset → charset
. ^ .	nat-pot	f	nat × nat → nat
. ∈ .	string-ops	p	char × string
. ∈ .	stringlist	p	string × stringlist
. ∈ .	charlist	p	char × charset
. ∈ .	charlist	p	char × charlist
. ∩ .	charlist	f	charset × charset → charset
. ∪ .	charlist	f	charlist × charlist → charlist
. ∪ .	charlist	f	charset × charset → charset
. ∪ .	stringlist	f	stringlist × stringlist → stringlist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	stringlist	p	stringlist × stringlist
. ⊆ .	charlist	p	charlist × charlist
. ⊆ .	charlist	p	charset × charset
. ⊆m .	stringlist	p	stringlist × stringlist
. ⊆m .	charlist	p	charlist × charlist
. ⊑ .	string-ops	p	string × string
. ⊑ .	charlist	p	charlist × charlist
. ⊑ .	stringlist	p	stringlist × stringlist
. ⊒ .	stringlist	p	stringlist × stringlist
. ⊒ .	charlist	p	charlist × charlist
[]	charlist	c	charlist
[]	stringlist	c	stringlist
{ . }	charlist	f	char → charset
∅	charlist	c	charset
2^ .	nat-pot	f	nat → nat
butlastn	stringlist	f	nat × stringlist → stringlist
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	stringlist	p	stringlist × stringlist
disj	charlist	p	charlist × charlist
downcase	string-ops	f	char → char
downcase	string-ops	f	string → string
downcase	string-ops	f	charlist → charlist
downcaseFirst	string-ops	f	string → string
dups	stringlist	p	stringlist
dups	charlist	p	charlist
fillfirst	charlist	f	nat × char × charlist → charlist
fillfirst	stringlist	f	nat × string × stringlist → stringlist
filter	stringlist	f	stringlist × stringlist → stringlist
filter	charlist	f	charlist × charlist → charlist
firstn	charlist	f	nat × charlist → charlist
firstn	stringlist	f	nat × stringlist → stringlist
frome	stringlist	f	stringlist × string → stringlist
frome	charlist	f	charlist × char → charlist
ins≤	stringlist	f	string × stringlist → stringlist
ins≤	charlist	f	char × charlist → charlist
l→s	string2list	f	charlist → string
lastn	charlist	f	nat × charlist → charlist
lastn	stringlist	f	nat × stringlist → stringlist
list2set	charlist	f	charlist → charset
log	nat-pot	f	nat × nat → nat
log2 .	nat-pot	f	nat → nat
m	nat-basic1	v	nat
merge	charlist	f	charlist × charlist → charlist
merge	stringlist	f	stringlist × stringlist → stringlist
mklist	charlist	f	char × nat → charlist
mklist	stringlist	f	string × nat → stringlist
n	nat-basic1	v	nat
n→s	string2nat	f	nat → string
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
ordered<	stringlist	p	stringlist
ordered<	charlist	p	charlist
ordered≤	stringlist	p	stringlist
ordered≤	charlist	p	charlist
perm	charlist	p	charlist × charlist
perm	stringlist	p	stringlist × stringlist
pos	string-less	f	char × string → nat
pos	charlist	f	char × charlist → nat
pos	stringlist	f	string × stringlist → nat
restn	stringlist	f	nat × stringlist → stringlist
restn	charlist	f	nat × charlist → charlist
rev	charlist	f	charlist → charlist
rev	stringlist	f	stringlist → stringlist
rmdup	charlist	f	charlist → charlist
rmdup	stringlist	f	stringlist → stringlist
s→l	string2list	f	string → charlist
s→n	string2nat	f	string → nat
set2list	charlist	f	charset → charlist
sort	stringlist	f	stringlist → stringlist
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
string-left-trim	string-ops	f	string × string → string
string-right-trim	string-ops	f	string × string → string
stringlist	stringlist	s
stringvar	string-append	v	string
stringvar0	string-append	v	string
strl	stringlist	v	stringlist
strl0	stringlist	v	stringlist
strl1	stringlist	v	stringlist
strl10	stringlist	v	stringlist
strl2	stringlist	v	stringlist
strl3	stringlist	v	stringlist
strl4	stringlist	v	stringlist
strl5	stringlist	v	stringlist
strl6	stringlist	v	stringlist
strl7	stringlist	v	stringlist
strl8	stringlist	v	stringlist
strl9	stringlist	v	stringlist
sublist	charlist	f	nat × nat × charlist → charlist
sublist	stringlist	f	nat × nat × stringlist → stringlist
substring	string-ops	f	string × nat × nat → string
trim-number	string-ops	f	string → string
upcase	string-ops	f	char → char
upcase	string-ops	f	string → string
upcase	string-ops	f	charlist → charlist
upcaseFirst	string-ops	f	string → string