Mercurial > hg > Members > atton > agda-proofs

comparison sandbox/TypeClass.agda @ 5:e8494d175afb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add sample for type class in Agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 15 Jan 2015 15:44:45 +0900
parents
children
comparison
equal deleted inserted replaced
4:fe1cf97997b9 5:e8494d175afb
1 -- type class example
2 -- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments?from=ReferenceManual.Non-canonicalImplicitArguments
3
4 open import Function
5 open import Data.Bool
6 open import Data.Nat
7
8 record Eq (t : Set) : Set where
9 field _==_ : t → t → Bool
10 _/=_ : t → t → Bool
11 a /= b = not $ a == b
12
13
14 open module EqWithImplicits {t : Set} {{eqT : Eq t}} = Eq eqT
15
16 instance
17 postulate
18 eqℕ : Eq ℕ
19 eqBool : Eq Bool
20
21
22 test = 5 == 3 ∧ true /= false