Imandra_prelude.Peano_nat
type t =
| Z
| S of t
val zero : t
val succ : t -> t
val of_int : int -> t
Turn this integer into a natural number. Negative integers map to zero.
val to_int : t -> int
Turn this natural number into a native integer.
val plus : t -> t -> t
Peano addition
val leq : t -> t -> bool
Comparison
val (=) : 'a -> 'a -> bool
val (<=) : t -> t -> bool
val (+) : t -> t -> t