CoPL Nat Derivation Rules

gistfile1.txt

module Nat where

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

data _plus_is_ : Nat -> Nat -> Nat -> Set where
  P-Zero : (m n : Nat) -> Z plus m is n
  P-Succ : (l m n : Nat) -> l plus m is n -> (S l) plus m is (S n)

data _times_is_ : Nat -> Nat -> Nat -> Set where
  T-Zero : (n : Nat) -> Z times n is Z
  T-Succ : (x y z w : Nat) -> x times y is z -> y plus z is w ->
           (S x) times y is w

q1 : Z plus Z is Z
q1 = P-Zero Z Z