Module prop::nat

Natural numbers with types.

Structs

• S
  Successor.
• Z
  Zero.

Enums

• NaN
  Not-a-number.

Constants

• _0
• _1
• _2
• _3

Traits

• Add
  Addition.
• Dec
  Decrement.
• EqNat
  Whether two natural numbers are equal.
• Lt
  Less than comparison.
• Nat
  Implemented for natural numbers.

Functions

• eq
  Check that one natural number is equal to the other.
• lt
  Check that one natural number is less than the other.
• lt_neq
  Provides a proof that the numbers are inequal.

Type Definitions

• One
  The one type.
• Three
  The three type.
• Two
  The two type.
• Zero
  The zero type.