Mercurial > hg > Members > atton > agda-proofs
view sandbox/TypeClass.agda @ 49:8031568638d0
Define composition of codesegment using subtype without constraint list
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 06 Jan 2017 06:29:51 +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