# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1421304285 -32400
# Node ID e8494d175afba36201128e1913851ad3fe6875fe
# Parent  fe1cf97997b987b42e848f2d4ad56179d5ba5a85
Add sample for type class in Agda

diff -r fe1cf97997b9 -r e8494d175afb sandbox/TypeClass.agda
--- /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