Signature symbols in this unit

Symbol	Specification	Kind	Type
. + .	int-basic2	f	Int × Int → Int
. + .	real-basic	f	Real × Real → Real
. +1	int-basic1	f	Int → Int
. - .	int-abs	f	Int × Int → Int
. - .	real-abs	f	Real × Real → Real
. -1	int-basic1	f	Int → Int
. < .	int-basic1	p	Int × Int
. < .	real-basic	p	Real × Real
. > .	int-abs	p	Int × Int
. > .	real-abs	p	Real × Real
. ≤ .	int-abs	p	Int × Int
. ≤ .	real-abs	p	Real × Real
. ≤ .	real-supinf	p	(Real → Bool) × Real
. ≤ .	real-supinf	p	Real × (Real → Bool)
. ≥ .	int-abs	p	Int × Int
. ≥ .	real-abs	p	Real × Real
. r	real-basic	f	Int → Real
~ .	int-abs	f	Int → Int
~ .	real-basic	f	Real → Real
Int	int-basic1	s
Real	real-basic	s
abs	int-abs	f	Int → Int
abs	real-abs	f	Real → Real
bounded≤	real-supinf	p	(Real → Bool)
bounded≥	real-supinf	p	(Real → Bool)
i	real-supinf	v	Int
inf	real-supinf	pf	(Real → Bool) → Real with λ rset. bounded≥(rset)
j	real-supinf	v	Int
r	real-supinf	v	Real
rset	real-supinf	v	Real → Bool
sup	real-supinf	pf	(Real → Bool) → Real with λ rset. bounded≤(rset)