Module Nat_2

module Nat_2: sig .. end

Provides type nat_2 : natural numbers (non-negative integers) along with basic operations involving them - Here the construction is inductive : a natural number is zero or one or the successor of the successor of a natural number.

type nat_2 =

`\|`	`Z`	`(*`	to represent zero	`*)`
`\|`	`Uno`	`(*`	to represent one	`*)`
`\|`	`S2 of nat_2`	`(*`	to represent the successor of the successor of a natural number	`*)`

Gives every natural number a unique representation.

val zero : unit -> nat_2

Constructs the natural number zero.

val one : unit -> nat_2

Constructs the natural number one.

val sucsuc : nat_2 -> nat_2

Constructs the successor of the successor of a natural number.

val is_zero : nat_2 -> bool

Tests whether a naturel number is zero.

val is_one : nat_2 -> bool

Tests whether a naturel number is one.

val prepre : nat_2 -> nat_2

Returns the predecessor of the predecessor of natural number greater than one.

Error if the number is zero or one.

val pr_nat : 'a -> nat_2 -> unit

val print_nat : nat_2 -> unit

Prints a string representation of a natural number.