type class

gistfile1.agda

module Test where

open import Data.Bool
open import Data.Char hiding (_==_)
open import Data.String hiding (_==_)

record Eq (A : Set) : Set₁ where
  field
    _==_ : A → A → Bool

open Eq {{...}}

EqChar : Eq Char
EqChar = record { _==_ = Data.Char._==_ }
EqString : Eq String
EqString = record { _==_ = Data.String._==_ }

test : Bool
test = (_==_ ⦃ EqChar ⦄ 'a' 'A') ∧ (_==_ ⦃ EqString ⦄ "foo" "foo")