Anonymous user
Proof: Difference between revisions
m
no edit summary
(update the task and agda example) |
mNo edit summary |
||
Line 39:
=={{header|ACL2}}==
3.1. using built-in natural numbers:
<lang Lisp>(thm (implies (and (evenp x) (evenp y))
(evenp (+ x y))))</lang>
Line 201 ⟶ 204:
=={{header|Coq}}==
1.1., 1.2, 2.1. and 3.1:
<lang coq>Inductive nat : Set :=
| O : nat
Line 241 ⟶ 247:
=={{header|Haskell}}==
Using [http://www.haskell.org/haskellwiki/GADT GADTs] and [http://www.haskell.org/haskellwiki/GHC/Type_families type families] it is possible to write
<lang haskell>{-# LANGUAGE TypeOperators, TypeFamilies, GADTs #-}
Line 247 ⟶ 253:
module Arith where
-- 1.1. Natural numbers.
data Z = Z
data S n = S n
-- 2.1. Addition.
infixl 6 :+
Line 259 ⟶ 265:
type instance (S m) :+ n = S (m :+ n)
--
data En :: * -> * where
Line 265 ⟶ 271:
Es :: En n -> En (S (S n))
--
sum_of_even_is_even :: En m -> En n -> En (m :+ n)
Line 280 ⟶ 286:
cong Refl = Refl
--
class AssocAdd m where
| |||