[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
#oc	stringlist	f	string × stringlist → nat
. '	string-append	f	char → string
. '	stringlist	f	string → stringlist
. + .	string-data	f	char × string → string
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	stringlist	f	stringlist × string → stringlist
. + .	stringlist	f	string × stringlist → stringlist
. + .	stringlist	f	stringlist × stringlist → stringlist
. ++ .	stringlist	f	stringlist × string → stringlist
. +1	nat-basic1	f	nat → nat
. +l .	stringlist	f	string × string → stringlist
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	stringlist	f	stringlist × nat → stringlist
. -1l .	stringlist	f	stringlist × string → stringlist
. -l .	stringlist	f	stringlist × string → stringlist
. .butlast	stringlist	f	stringlist → stringlist
. .char1	string-data	f	string → char
. .first	stringlist	f	stringlist → string
. .last	stringlist	f	stringlist → string
. .rest	stringlist	f	stringlist → stringlist
. .rstring	string-data	f	string → string
. < .	stringlist	p	stringlist × stringlist
. < .	string-less	p	char × char
. < .	nat-basic1	p	nat × nat
. < .	string-less	p	string × string
. > .	nat	p	nat × nat
. [ . ]	stringlist	f	stringlist × nat → string
. [ . ]	stringlist	f	stringlist × nat × string → stringlist
. \ .	stringlist	f	stringlist × stringlist → stringlist
. ∈ .	stringlist	p	string × stringlist
. ∪ .	stringlist	f	stringlist × stringlist → stringlist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	stringlist	p	stringlist × stringlist
. ⊆m .	stringlist	p	stringlist × stringlist
. ⊑ .	stringlist	p	stringlist × stringlist
. ⊒ .	stringlist	p	stringlist × stringlist
[]	stringlist	c	stringlist
butlastn	stringlist	f	nat × stringlist → stringlist
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
disj	stringlist	p	stringlist × stringlist
dups	stringlist	p	stringlist
fillfirst	stringlist	f	nat × string × stringlist → stringlist
filter	stringlist	f	stringlist × stringlist → stringlist
firstn	stringlist	f	nat × stringlist → stringlist
frome	stringlist	f	stringlist × string → stringlist
ins≤	stringlist	f	string × stringlist → stringlist
lastn	stringlist	f	nat × stringlist → stringlist
m	nat-basic1	v	nat
merge	stringlist	f	stringlist × stringlist → stringlist
mklist	stringlist	f	string × nat → stringlist
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
ordered<	stringlist	p	stringlist
ordered≤	stringlist	p	stringlist
perm	stringlist	p	stringlist × stringlist
pos	string-less	f	char × string → nat
pos	stringlist	f	string × stringlist → nat
restn	stringlist	f	nat × stringlist → stringlist
rev	stringlist	f	stringlist → stringlist
rmdup	stringlist	f	stringlist → stringlist
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
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	stringlist	f	nat × nat × stringlist → stringlist