[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
# .	classnames	f	classnameset → nat
# .	classnames	f	classnames → nat
#oc	classnames	f	classname × classnames → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	storekey	f	int → storekey
. '	string-append	f	char → string
. '	storekey	f	fieldspec → storekey
. '	classnames	f	classname → classnames
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	string-data	f	char × string → string
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	classnames	f	classname × classname → classnames
. + .	int-basic2	f	int × int → int
. + .	classnames	f	classnames × classname → classnames
. + .	classnames	f	classname × classnames → classnames
. + .	classnames	f	classnames × classnames → classnames
. ++ .	classnames	f	classnameset × classname → classnameset
. ++ .	classnames	f	classnames × classname → classnames
. +1	nat-basic1	f	nat → nat
. +1	int-basic1	f	int → int
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -- .	refkey	f	reference × storekey → refkey
. -- .	classnames	f	classnameset × classname → classnameset
. -1	nat-basic1	f	nat → nat
. -1	int-basic1	f	int → int
. -1l .	classnames	f	classnames × nat → classnames
. -1l .	classnames	f	classnames × classname → classnames
. -l .	classnames	f	classnames × classname → classnames
. .butlast	classnames	f	classnames → classnames
. .butmax	classnames	f	classnameset → classnameset
. .butmin	classnames	f	classnameset → classnameset
. .char1	string-data	f	string → char
. .class	fieldspec	f	fieldspec → classname
. .class	classname	f	string → classname
. .class	javatype	f	javatype → classname
. .class	classname	f	classname → string
. .field	fieldname	f	string → fieldname
. .field	fieldname	f	fieldname → string
. .field	fieldspec	f	fieldspec → fieldname
. .first	classnames	f	classnames → classname
. .fs	storekey	f	storekey → fieldspec
. .index	storekey	f	storekey → int
. .jtclass	typefuns	f	javatype → classname
. .jtdims	typefuns	f	javatype → int
. .jtelemtype	typefuns	f	javatype → javatype
. .key	refkey	f	refkey → storekey
. .last	classnames	f	classnames → classname
. .max	classnames	f	classnameset → classname
. .min	classnames	f	classnameset → classname
. .ref	refkey	f	refkey → reference
. .rest	classnames	f	classnames → classnames
. .rstring	string-data	f	string → string
. .type	fieldspec	f	fieldspec → javatype
. .type	javatype	f	javatype → javatype
. / .	nat-div	f	nat × nat → nat
. / .	int-div	f	int × int → int
. < .	reference	p	reference × reference
. < .	classnames	p	classnameset × classname
. < .	nat-basic1	p	nat × nat
. < .	classnames	p	classname × classnameset
. < .	classnames	p	classnames × classnames
. < .	string-less	p	string × string
. < .	string-less	p	char × char
. < .	int-basic1	p	int × int
. <_1 .	classnamefuns	p	classname × classname
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. [ . ]	classnames	f	classnames × nat → classname
. [ . ]	classnames	f	classnames × nat × classname → classnames
. \ .	classnames	f	classnameset × classnameset → classnameset
. \ .	classnames	f	classnames × classnames → classnames
. ≤ .	typefuns	p	javatype × javatype
. ≤ .	nat	p	nat × nat
. ≤ .	classnamefuns	p	classname × classname
. ≤ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ∈ .	classnames	p	classname × classnameset
. ∈ .	classnames	p	classname × classnames
. ∪ .	classnames	f	classnames × classnames → classnames
. ∪ .	classnames	f	classnameset × classnameset → classnameset
. ∩ .	classnames	f	classnameset × classnameset → classnameset
. ⊆ .	classnames	p	classnameset × classnameset
. ⊆ .	classnames	p	classnames × classnames
. ⊆m .	classnames	p	classnames × classnames
. ⊑ .	classnames	p	classnames × classnames
. ⊒ .	classnames	p	classnames × classnames
. l< .	classnamefuns	p	classname × classname
[]	classnames	c	classnames
{ . }	classnames	f	classname → classnameset
~ .	int-abs	f	int → int
∅	classnames	c	classnameset
abs	int-abs	f	int → int
abstract_type	javatype	c	javatype
boolean_type	javatype	c	javatype
butlastn	classnames	f	nat × classnames → classnames
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
claset	classnames	v	classnameset
claset0	classnames	v	classnameset
claset1	classnames	v	classnameset
claset2	classnames	v	classnameset
class	classname	v	classname
class+∃	typefuns	p	string × classname
class∃	typefuns	p	string × classname
class0	classname	v	classname
class1	classname	v	classname
class2	classname	v	classname
class3	classname	v	classname
classes	classnames	v	classnames
classes0	classnames	v	classnames
classes1	classnames	v	classnames
classes10	classnames	v	classnames
classes2	classnames	v	classnames
classes3	classnames	v	classnames
classes4	classnames	v	classnames
classes5	classnames	v	classnames
classes6	classnames	v	classnames
classes7	classnames	v	classnames
classes8	classnames	v	classnames
classes9	classnames	v	classnames
classname	classname	s
classnames	classnames	s
classnameset	classnames	s
disj	classnames	p	classnames × classnames
double_type	javatype	c	javatype
dups	classnames	p	classnames
fieldname	fieldname	s
fieldspec	fieldspec	s
fieldvar	fieldname	v	fieldname
fieldvar0	fieldname	v	fieldname
fieldvar1	fieldname	v	fieldname
fieldvar2	fieldname	v	fieldname
fieldvar3	fieldname	v	fieldname
fillfirst	classnames	f	nat × classname × classnames → classnames
filter	classnames	f	classnames × classnames → classnames
firstn	classnames	f	nat × classnames → classnames
float_type	javatype	c	javatype
frome	classnames	f	classnames × classname → classnames
fs	fieldspec	v	fieldspec
fs0	fieldspec	v	fieldspec
fs1	fieldspec	v	fieldspec
has_classtype	typefuns	p	javatype
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
ins≤	classnames	f	classname × classnames → classnames
int	int-basic1	s
int_type	javatype	c	javatype
interface∃	typefuns	p	string × classname
is_abstract	typefuns	p	classname
is_arraytype	javatype	p	javatype
is_classtype	javatype	p	javatype
is_fskey	storekey	p	storekey
is_indexkey	storekey	p	storekey
is_predefined_class	predefined	p	classname
is_primtype	typefuns	p	javatype
is_reftype	typefuns	p	javatype
is_subclass	typefuns	p	classname × classnames × classname
is_subtype	typefuns	p	string × javatype × javatype
is_subtype	typefuns	p	javatype × classnames × javatype
is_subtype	typefuns	p	javatype × javatype × classnameset
is_void_type	javatype	p	javatype
j	int-basic1	v	int
j0	int-basic1	v	int
javatype	javatype	s
jvmref	reference	c	reference
lastn	classnames	f	nat × classnames → classnames
list2set	classnames	f	classnames → classnameset
long_type	javatype	c	javatype
m	nat-basic2	v	nat
merge	classnames	f	classnames × classnames → classnames
mkarraytype	javatype	f	javatype → javatype
mkclasstype	javatype	f	classname → javatype
mkfs	fieldspec	f	classname × javatype × fieldname → fieldspec
mklist	classnames	f	classname × nat → classnames
mktype_from_dims	typefuns	f	javatype × int → javatype
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
next	reference	f	reference → reference
ordered<	classnames	p	classnames
ordered≤	classnames	p	classnames
perm	classnames	p	classnames × classnames
pos	string-less	f	char × string → nat
pos	classnames	f	classname × classnames → nat
predef_superClass	predefined	f	classname → classname
predef_supers	predefined	f	classname → classnames
predefined_classes	predefined	c	classnames
r	reference	v	reference
r0	reference	v	reference
r1	reference	v	reference
r2	reference	v	reference
reference	reference	s
refkey	refkey	s
restn	classnames	f	nat × classnames → classnames
rev	classnames	f	classnames → classnames
rk	refkey	v	refkey
rk0	refkey	v	refkey
rk1	refkey	v	refkey
rk2	refkey	v	refkey
rmdup	classnames	f	classnames → classnames
set2list	classnames	f	classnameset → classnames
short_type	javatype	c	javatype
sk	storekey	v	storekey
sk0	storekey	v	storekey
sk1	storekey	v	storekey
sortedchars	string-less	c	string
storekey	storekey	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
stringvar	string-append	v	string
stringvar0	string-append	v	string
sublist	classnames	f	nat × nat × classnames → classnames
tdname+∃	typefuns	p	string × classname
tdname∃	typefuns	p	string × classname
this	reference	v	reference
ty	javatype	v	javatype
ty0	javatype	v	javatype
ty1	javatype	v	javatype
ty2	javatype	v	javatype
type∃	typefuns	p	string × javatype
void_type	javatype	c	javatype