Mercurial > hg > Members > atton > agda-proofs

changeset 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 fe1cf97997b9
children 90abb3f53c03
files sandbox/TypeClass.agda
diffstat 1 files changed, 22 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sandbox/TypeClass.agda	Thu Jan 15 15:44:45 2015 +0900
@@ -0,0 +1,22 @@
+-- type class example
+-- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments?from=ReferenceManual.Non-canonicalImplicitArguments
+
+open import Function
+open import Data.Bool
+open import Data.Nat
+
+record Eq (t : Set) : Set where
+  field _==_ : t → t → Bool
+  _/=_ : t → t → Bool
+  a /= b = not $ a == b
+
+
+open module EqWithImplicits {t : Set} {{eqT : Eq t}} = Eq eqT
+
+instance
+   postulate  
+     eqℕ    : Eq ℕ
+     eqBool : Eq Bool
+
+
+test = 5 == 3 ∧ true /= false