[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
# .	bitlista	f	bitlist → nat
#oc	bitlista	f	bool × bitlist → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	string-append	f	char → string
. '	bitlista	f	bool → bitlist
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	string-data	f	char × string → string
. + .	bitlista	f	bool × bitlist → bitlist
. + .	bitlista	f	bitlist × bitlist → bitlist
. + .	bitlista	f	bool × bool → bitlist
. + .	bitlista	f	bitlist × bool → bitlist
. ++ .	bitlista	f	bitlist × bool → bitlist
. +1	int-basic1	f	int → int
. +1	bitopsaux	f	bitlist → bitlist
. +1	nat-basic1	f	nat → nat
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. -1l .	bitlista	f	bitlist × nat → bitlist
. -1l .	bitlista	f	bitlist × bool → bitlist
. -l .	bitlista	f	bitlist × bool → bitlist
. .butlast	bitlista	f	bitlist → bitlist
. .char1	string-data	f	string → char
. .first	bitlista	p	bitlist
. .int	float	f	float → int
. .int	float	f	double → int
. .last	bitlista	p	bitlist
. .rest	bitlista	f	bitlist → bitlist
. .rstring	string-data	f	string → string
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	string-less	p	char × char
. < .	string-less	p	string × string
. < .	bitlista	p	bitlist × bitlist
. < .	nat-basic1	p	nat × nat
. < .	int-basic1	p	int × int
. << .	intops	f	int × int → int
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. >> .	intops	f	int × int → int
. [ . ]	bitlista	f	bitlist × nat × bool → bitlist
. [ . ]	bitlista	p	bitlist × nat
. \ .	bitlista	f	bitlist × bitlist → bitlist
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ∈ .	bitlista	p	bool × bitlist
. ∈bint	byte	p	int
. ∈byte	byte	p	int
. ∈long	byte	p	int
. ∈short	byte	p	int
. ∪ .	bitlista	f	bitlist × bitlist → bitlist
. ⊆ .	bitlista	p	bitlist × bitlist
. ⊆m .	bitlista	p	bitlist × bitlist
. ⊑ .	bitlista	p	bitlist × bitlist
. ⊒ .	bitlista	p	bitlist × bitlist
. i<< .	intops	f	int × int → int
. i>> .	intops	f	int × int → int
. i>>> .	intops	f	int × int → int
. l<< .	intops	f	int × int → int
. l>> .	intops	f	int × int → int
. l>>> .	intops	f	int × int → int
>>>	intops	f	nat × int × int → int
[]	bitlista	c	bitlist
~ .	int-abs	f	int → int
0b	byte	c	byte
0bi	byte	c	bint
0d	float	c	double
0f	float	c	float
0l	byte	c	long
0s	byte	c	short
abs	int-abs	f	int → int
b2bi	byte	f	byte → bint
b2i	byte	f	byte → int
b2s	byte	f	byte → short
band	intops	f	int × int → int
bcompl	intops	f	int → int
bi	byte	v	bint
bi2b	byte	f	bint → byte
bi2i	byte	f	bint → int
bi2s	byte	f	bint → short
bint	byte	s
bitlist	bitlista	s
bits	bitlista	v	bitlist
bits0	bitlista	v	bitlist
bits1	bitlista	v	bitlist
bits10	bitlista	v	bitlist
bits2	bitlista	v	bitlist
bits2int	int2bits	f	bitlist → int
bits2uint	int2bits	f	bitlist → int
bits3	bitlista	v	bitlist
bits4	bitlista	v	bitlist
bits5	bitlista	v	bitlist
bits6	bitlista	v	bitlist
bits7	bitlista	v	bitlist
bits8	bitlista	v	bitlist
bits9	bitlista	v	bitlist
bitsand	intops	f	bitlist × bitlist → bitlist
bitsinvert	bitopsaux	f	bitlist → bitlist
bitsor	intops	f	bitlist × bitlist → bitlist
bitsxor	intops	f	bitlist × bitlist → bitlist
bj	byte	v	bint
bool	bool	s
boolvar	bool	v	bool
boolvar0	bool	v	bool
boolvar1	bitlista	v	bool
boolvar2	bitlista	v	bool
bor	intops	f	int × int → int
butlastn	bitlista	f	nat × bitlist → bitlist
bxor	intops	f	int × int → int
by	byte	v	byte
byi	byte	v	byte
byj	byte	v	byte
byte	byte	s
cast	intops	f	int × int → int
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	bitlista	p	bitlist × bitlist
double	float	s
doublevar	float	v	double
dups	bitlista	p	bitlist
even	int-min	p	int
fillfirst	bitlista	f	nat × bool × bitlist → bitlist
fillsgn	bitopsaux	f	nat × bitlist → bitlist
filter	bitlista	f	bitlist × bitlist → bitlist
firstn	bitlista	f	nat × bitlist → bitlist
fix	bitopsaux	f	nat × bitlist → bitlist
float	float	s
floatvar	float	v	float
frome	bitlista	f	bitlist × bool → bitlist
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
i2b	byte	f	int → byte
i2bi	byte	f	int → bint
i2l	byte	f	int → long
i2s	byte	f	int → short
int	int-basic1	s
int2bits	int2bits	f	int → bitlist
j	int-basic1	v	int
j0	int-basic1	v	int
l2i	byte	f	long → int
lastn	bitlista	f	nat × bitlist → bitlist
lo	byte	v	long
loi	byte	v	long
loj	byte	v	long
long	byte	s
m	nat-basic2	v	nat
max	int-min	f	int × int → int
min	int-min	f	int × int → int
mkdouble	float	f	string → double
mkfloat	float	f	string → float
mklist	bitlista	f	bool × nat → bitlist
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
odd	int-min	p	int
perm	bitlista	p	bitlist × bitlist
pos	string-less	f	char × string → nat
pos	bitlista	f	bool × bitlist → nat
restn	bitlista	f	nat × bitlist → bitlist
rev	bitlista	f	bitlist → bitlist
rmdup	bitlista	f	bitlist → bitlist
s2b	byte	f	short → byte
s2bi	byte	f	short → bint
s2i	byte	f	short → int
sgn	int-min	f	int → int
sgn	bitopsaux	f	bitlist → bitlist
sho	byte	v	short
shoi	byte	v	short
shoj	byte	v	short
short	byte	s
shortOverflow	byte	p	int
sortedchars	string-less	c	string
sqrt	int-square	f	int → int
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	bitlista	f	nat × nat × bitlist → bitlist
ub2i	byte	f	byte → int
uint2bits	int2bits	f	int → bitlist
us2i	byte	f	short → int