Anonymous user
Proof: Difference between revisions
→Examples
m (→{{header|Ada}}: Corrected typo) |
|||
Line 144:
<font color="#00008b">assumption</font>.
<font color="#a020f0">Qed</font>.
=={{header|Omega}}==
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)
|