[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
. '	string-append	f	char → string
. + .	string-data	f	char × string → string
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. .char1	string-data	f	string → char
. .class	javatype	f	javatype → classname
. .class	classname	f	classname → string
. .class	classname	f	string → classname
. .rstring	string-data	f	string → string
. .type	javatype	f	javatype → javatype
. < .	string-less	p	char × char
. < .	string-less	p	string × string
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
abstract_type	javatype	c	javatype
boolean_type	javatype	c	javatype
byte_type	javatype	c	javatype
char	char	s
char	char	v	char
char_type	javatype	c	javatype
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
class	classname	v	classname
class0	classname	v	classname
class1	classname	v	classname
class2	classname	v	classname
class3	classname	v	classname
classname	classname	s
double_type	javatype	c	javatype
float_type	javatype	c	javatype
int_type	javatype	c	javatype
is_arraytype	javatype	p	javatype
is_classtype	javatype	p	javatype
is_void_type	javatype	p	javatype
javatype	javatype	s
long_type	javatype	c	javatype
m	nat-basic2	v	nat
mkarraytype	javatype	f	javatype → javatype
mkclasstype	javatype	f	classname → javatype
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pos	string-less	f	char × string → nat
short_type	javatype	c	javatype
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
ty	javatype	v	javatype
ty0	javatype	v	javatype
ty1	javatype	v	javatype
ty2	javatype	v	javatype
void_type	javatype	c	javatype