Module Nat_3

module Nat_3: sig .. end

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

type nat_3 =

`\|`	`Z`	`(*`	to represent zero	`*)`
`\|`	`TTNZ of nat_3`	`(*`	to represent two times a non-zero natural number	`*)`
`\|`	`STT of nat_3`	`(*`	to represent the successor of two times a natural number	`*)`

Gives every natural number a unique representation.

val zero : unit -> nat_3

Constructs the natural number zero.

val d0 : nat_3 -> nat_3

Constructs the natural number that is two times a non-zero natural number.

Error if the number is zero.

val d1 : nat_3 -> nat_3

Constructs the natural number that is the successor of two times a natural number.

val is_even_non_zero : nat_3 -> bool

Test whether a natural number is even and non-zero.

val is_odd : nat_3 -> bool

Test whether a natural number is odd.

val inv_d0 : nat_3 -> nat_3

The inverse of the function d0.

Error if it is applied to zero or an odd natural number.

val inv_d1 : nat_3 -> nat_3

The inverse of the function d1.

Error if it is applied to an even natural number.

val pr_nat : 'a -> nat_3 -> unit

val print_nat : nat_3 -> unit

Prints a string representation of a natural number.