[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
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. * .	decimal-simple-ops	f	decimal × decimal → decimal
. * .	nat-mult	f	nat × nat → nat
. * .	int-mult	f	int × int → int
. + .	int-basic2	f	int × int → int
. + .	decimal-simple-ops	f	decimal × decimal → decimal
. + .	nat-basic2	f	nat × nat → nat
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. - .	decimal-simple-ops	f	decimal × decimal → decimal
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. .int	decimal	f	decimal → int
. .scale	decimal	f	decimal → int
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	decimal-simple-ops	p	decimal × decimal
. < .	int-basic1	p	int × int
. < .	nat-basic1	p	nat × nat
. > .	decimal-simple-ops	p	decimal × decimal
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. ^ .	int-pot	f	int × int → int
. ^2	int-square	f	int → int
. \| .	int-gcd	p	int × int
. ≤ .	decimal-simple-ops	p	decimal × decimal
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	decimal-simple-ops	p	decimal × decimal
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
~ .	int-abs	f	int → int
~ .	decimal-simple-ops	f	decimal → decimal
0_dec	decimal-simple-ops	c	decimal
1_dec	decimal-simple-ops	c	decimal
abs	int-abs	f	int → int
abs	decimal-simple-ops	f	decimal → decimal
dec	decimal	v	decimal
dec_i	decimal	v	decimal
dec_i0	decimal	v	decimal
dec_j	decimal	v	decimal
dec_j0	decimal	v	decimal
dec0	decimal	v	decimal
dec1	decimal	v	decimal
dec2	decimal	v	decimal
dec2int	decimal	f	decimal → int
decimal	decimal	s
even	int-min	p	int
gcd	int-gcd	f	int × int → int
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
inc	decimal	f	decimal → decimal
int	int-basic1	s
isSquare	int-square	p	int
j	int-basic1	v	int
j0	int-basic1	v	int
m	nat-basic1	v	nat
max	int-min	f	int × int → int
max_prime_divisor	int-gcd	f	int → int
maxScale	decimal	f	int → int
min	int-min	f	int × int → int
mkDecimal	decimal	f	int × int → decimal
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
prime	int-gcd	p	int
sgn	int-min	f	int → int
sqrt	int-square	f	int → int
truncate	decimal	f	decimal × int → decimal