[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
# .	bitlista	f	bitlist → nat
#oc	bitlista	f	bool × bitlist → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	bitlista	f	bool → bitlist
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	bitlista	f	bool × bool → bitlist
. + .	bitlista	f	bool × bitlist → bitlist
. + .	bitlista	f	bitlist × bool → bitlist
. + .	bitlista	f	bitlist × bitlist → 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
. .first	bitlista	p	bitlist
. .last	bitlista	p	bitlist
. .rest	bitlista	f	bitlist → bitlist
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	bitlista	p	bitlist × bitlist
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. [ . ]	bitlista	p	bitlist × nat
. [ . ]	bitlista	f	bitlist × nat × bool → bitlist
. \ .	bitlista	f	bitlist × bitlist → bitlist
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. ∈ .	bitlista	p	bool × bitlist
. ∪ .	bitlista	f	bitlist × bitlist → bitlist
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ⊆ .	bitlista	p	bitlist × bitlist
. ⊆m .	bitlista	p	bitlist × bitlist
. ⊑ .	bitlista	p	bitlist × bitlist
. ⊒ .	bitlista	p	bitlist × bitlist
[]	bitlista	c	bitlist
~ .	int-abs	f	int → int
abs	int-abs	f	int → int
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
bitsinvert	bitopsaux	f	bitlist → bitlist
bool	bool	s
boolvar	bool	v	bool
boolvar0	bool	v	bool
boolvar1	bitlista	v	bool
boolvar2	bitlista	v	bool
butlastn	bitlista	f	nat × bitlist → bitlist
disj	bitlista	p	bitlist × bitlist
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
frome	bitlista	f	bitlist × bool → bitlist
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
int	int-basic1	s
int2bits	int2bits	f	int → bitlist
isSquare	int-square	p	int
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	bitlista	f	nat × bitlist → bitlist
m	nat-basic1	v	nat
max	int-min	f	int × int → int
min	int-min	f	int × int → int
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	bitlista	f	bool × bitlist → nat
restn	bitlista	f	nat × bitlist → bitlist
rev	bitlista	f	bitlist → bitlist
rmdup	bitlista	f	bitlist → bitlist
sgn	bitopsaux	f	bitlist → bitlist
sgn	int-min	f	int → int
sqrt	int-square	f	int → int
sublist	bitlista	f	nat × nat × bitlist → bitlist
uint2bits	int2bits	f	int → bitlist