Mercurial > hg > Members > atton > agda-proofs
view sandbox/TypeClass.agda @ 16:62dfa11a8629
Define tuple compose
author | atton |
---|---|
date | Sat, 17 Dec 2016 07:07:01 +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