Proof: Difference between revisions
m
Alphabetized
m (→{{header|Twelf}}: Syntax highliter doesn't support twelf) |
m (Alphabetized) |
||
Line 102:
end Evens;
=={{header|Agda2}}==▼
<agda2>▼
module Arith where▼
data Nat : Set where▼
zero : Nat▼
suc : Nat -> Nat▼
_+_ : Nat -> Nat -> Nat▼
zero + n = n▼
suc m + n = suc (m + n)▼
data Even : Nat -> Set where▼
even_zero : Even zero▼
even_suc_suc : {n : Nat} -> Even n -> Even (suc (suc n))▼
_even+_ : {m n : Nat} -> Even m -> Even n -> Even (m + n)▼
even_zero even+ en = en▼
even_suc_suc em even+ en = even_suc_suc (em even+ en)▼
</agda2>▼
=={{header|Coq}}==
Line 155 ⟶ 178:
even_plus EZ en = en
even_plus (ES em) en = ES (even_plus em en)
▲=={{header|Agda2}}==
▲<agda2>
▲module Arith where
▲data Nat : Set where
▲ zero : Nat
▲ suc : Nat -> Nat
▲_+_ : Nat -> Nat -> Nat
▲zero + n = n
▲suc m + n = suc (m + n)
▲data Even : Nat -> Set where
▲ even_zero : Even zero
▲ even_suc_suc : {n : Nat} -> Even n -> Even (suc (suc n))
▲_even+_ : {m n : Nat} -> Even m -> Even n -> Even (m + n)
▲even_zero even+ en = en
▲even_suc_suc em even+ en = even_suc_suc (em even+ en)
▲</agda2>
=={{header|Twelf}}==
| |||