Module Nat_1

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 nat_1 =

`\|`	`Z`	`(*`	to represent zero	`*)`
`\|`	`S of nat_1`	`(*`	to represent the successor of a natural number	`*)`

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 pr_nat : 'a -> nat_1 -> unit

val print_nat : nat_1 -> unit

Prints a string representation of a natural number.