Mercurial > hg > Members > atton > agda-proofs
view sandbox/TypeClass.agda @ 14:31b1b7cc43cd
Prove state is functor
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 May 2016 16:31:56 +0900 |
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