Proof: Difference between revisions

data Even :: Nat ~> *0 where

EZ:: Even Z

ES:: Even n -> Even (S (S n))

plus:: Nat ~> Nat ~> Nat

{plus Z m} = m

{plus (S n) m} = S {plus n m}

even_plus:: Even m -> Even n -> Even {plus m n}

even_plus EZ en = en

even_plus (ES em) en = ES (even_plus em en)