Mercurial > hg > Members > atton > agda-proofs
view sandbox/TypeClass.agda @ 21:afb2304be45b
Merge 20:d924de5deb70
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 18 Dec 2016 08:13:08 +0000 |
parents | e8494d175afb |
children |
line wrap: on
line source
-- 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