Mercurial > hg > Members > atton > agda-proofs
view sandbox/TypeClass.agda @ 60:bd428bd6b394
Trying define n-push/n-pop
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 14 Jan 2017 00:00:40 +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