Module Imandra_prelude.Peano_nat

Natural numbers

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