Proof: Difference between revisions
→{{header|Agda}}: Updated Agda example
(→{{header|Agda}}: Updated Agda example) |
(→{{header|Agda}}: Updated Agda example) |
||
Line 44:
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
-- 1.2. The even natural numbers.
Line 56:
data 2×ℕ+1 : ℕ → Set where
one : 2×ℕ+1 (suc zero)
2+
-- 2.1. The rule of addition.
Line 63:
--
infixl 6 _+_
_+_ : (k : ℕ) → (n : ℕ) → ℕ
zero + n = n
(suc m) + n = suc (m + n)
-- 3.1. Sum of any two even numbers is even.
Line 202:
even+even≢odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ+1 (m + n)
even+even≢odd zero₁ zero₁ ()
even+even≢odd zero₁ (2+ n) (2+₁ m+n) = even+even≢odd zero₁ n m+n
even+even≢odd (2+ m) n (2+₁ m+n) = even+even≢odd m n m+n
-- 4.2.
| |||