[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	f	string → nat
. '	string	f	char → string
. + .	nat-basic	f	nat × nat → nat
. + .	string	f	char × string → string
. + .	string	f	string × string → string
. + .	string	f	string × char → string
. ++ .	string	f	string × char → string
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -l .	string	f	string × char → string
. -p .	string	f	string × nat → string
. .butlast	string	pf	string → string with λ x. x ≠ ""
. .char1	string	pf	string → char with λ x. x ≠ ""
. .last	string	pf	string → char with λ x. x ≠ ""
. .rstring	string	pf	string → string with λ x. x ≠ ""
. < .	nat-basic	p	nat × nat
. < .	string-less	p	string × string
. < .	string-less	p	char × char
. > .	nat	p	nat × nat
. [ . ]	string	pf	string × nat → char with λ x, n. n < # x
. [ . ]	string	pf	string × nat × char → string with λ x, n, a. n < # x
. ∈ .	string	p	char × string
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	string	p	string × string
. ⊒ .	string	p	string × string
⊏	string	p	string × string
butlastn	string	pf	nat × string → string with λ n, x. n ≤ # x
char	char	s
char	string-less	v	char
disj	string	p	string × string
dups	string	p	string
fillfirst	string	f	nat × char × string → string
firstn	string	pf	nat × string → string with λ n, x. n ≤ # x
frome	string	f	string × char → string
lastn	string	pf	nat × string → string with λ n, x. n ≤ # x
mklist	string	f	char × nat → string
nat	nat-basic	s
pos	string	f	char × string → nat
restn	string	pf	nat × string → string with λ n, x. n ≤ # x
rev	string	f	string → string
rmdup	string	f	string → string
sortedchars	string-less	c	string
str	string-less	v	string
string	string	s
sublist	string	pf	nat × nat × string → string with λ n, m, x. n + m ≤ # x