view sandbox/TypeClass.agda @ 25:da78bb99d654

Embed function body to codesegment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 02:36:46 +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