20071012-2

module Nat where

data Nat : Set where

  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat zero + m = m succ n + m = succ (n + m)

infixl 60 _+_

natrec : (C : Nat -> Set) -> (C zero) -> ((m : Nat) -> C m -> C (succ m)) ->

         (n : Nat) -> C n

natrec C p h zero = p natrec C p h (succ n) = h n (natrec C p h n)

plus : Nat -> Nat -> Nat plus n m = natrec (\x -> Nat) m (\x y -> succ y) n

data _==_ {A : Set} : A -> A -> Set where

  refl : (x : A) -> x == x

eq-succ : (n m : Nat) -> n == m -> succ n == succ m eq-succ .n .n (refl n) = {!refl (succ n)!} -- refl (succ n)

eq-plus : (n m : Nat) -> n + m == plus n m eq-plus zero m = refl m eq-plus (succ n) m = eq-succ {!(n + m)!} (plus n m) {! !}

Fixed. -- Ulf