Nat

Nat package contains inductive data type definition representing Peano arithmetic.

data nat = zero | suc (a: nat)

zero

zero construction represent lowest nat number.

> let a: nat = zero in a
EVAL: zero

suc

suc constructor defines next nat number.

> let a: nat = suc zero in a
EVAL: suc zero

Generics

pred: nat -> nat

Returns a nat predecessor.

> pred (suc zero)
EVAL: zero

add (m: nat) : nat -> nat

Returns an addendum.

Instances

equalNat : nat -> nat -> bool nat_instance : eq = (nat, equalNat)

Theorems

add_zero : (n : nat) -> Path nat (add zero n) n add_suc (a:nat) : (n : nat) -> Path nat (add (suc a) n) (suc (add a n)) add_comm (a : nat) : (n : nat) -> Path nat (add a n) (add n a) assocAdd (a b:nat) : (c:nat) -> Path nat (add a (add b c)) (add (add a b) c) sucInj (n m : nat) (p : Path nat (suc n) (suc m)) : Path nat n m add_comm3 (a b c : nat) : Path nat (add a (add b c)) (add c (add b a)) caseNat (A : U) (a0 aS : A) : nat -> A caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) natDec : (n m:nat) -> dec (Path nat n m) natSet : isSet nat