Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	stringset	f	stringset → nat
. + .	string-data	f	char × string → string
. + .	nat-basic2	f	nat × nat → nat
. ++ .	stringset	f	stringset × string → stringset
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	stringset	f	stringset × string → stringset
. -1	nat-basic1	f	nat → nat
. .char1	string-data	f	string → char
. .rstring	string-data	f	string → string
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. \ .	stringset	f	stringset × stringset → stringset
. ∈ .	stringset	p	string × stringset
. ∩ .	stringset	f	stringset × stringset → stringset
. ∪ .	stringset	f	stringset × stringset → stringset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	stringset	p	stringset × stringset
{ . }	stringset	f	string → stringset
∅	stringset	c	stringset
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
m	nat-basic1	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
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
strings	stringset	v	stringset
strings0	stringset	v	stringset
strings1	stringset	v	stringset
strings2	stringset	v	stringset
stringset	stringset	s