module Nat_1: sig .. end
Provides type nat_1 : natural numbers (non-negative integers)
along with basic operations involving them - Here the construction is inductive :
a natural number is either zero or the successor of a natural number.
type
Gives every natural number a unique representation.
val zero : unit -> nat_1
Constructs the natural number zero.
val suc : nat_1 -> nat_1
Constructs the successor of a natural number.
val is_zero : nat_1 -> bool
Tests whether a naturel number is zero.
val pre : nat_1 -> nat_1
Returns the predecessor of non-zero natural number.
- Error if the number is zero.
val print_nat : nat_1 -> unit
Prints a string representation of a natural number.