Arithmetic specification #

Integer and real arithmetic, the comparisons, the transcendental functions, and the predicates over them.

Division and modulus come in two flavours: the plain ones leave the result on a zero divisor unspecified, the Total ones define it — zero for a division, the dividend for intModTotal — and are experimental in cvc5. Integer division and modulus are Euclidean, as Lean's own / and % on Int are.