Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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")
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement