blob: 4a7b84f72404ad57f05133d14adaee029b21962b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
module B.Prelude.Eq where
import Data.Bool as Bool
open Bool using (Bool)
import Data.Char as Char
open Char using (Char)
import Data.Nat as ℕ
open ℕ using (ℕ)
open import Function using (_$_)
import Level
open Level using (_⊔_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary using (DecSetoid)
record Eq {c} {ℓ} (t : Set c) : Set (Level.suc $ c ⊔ ℓ) where
field
decSetoid : DecSetoid c ℓ
_≟_ = DecSetoid._≟_ decSetoid
_==_ : DecSetoid.Carrier decSetoid
→ DecSetoid.Carrier decSetoid
→ Bool
x == y = ⌊ x ≟ y ⌋
open Eq ⦃...⦄ public
instance
Eq-Bool : Eq Bool
Eq-Bool = record { decSetoid = Bool.decSetoid }
Eq-Char : Eq Char
Eq-Char = record { decSetoid = Char.decSetoid }
-- TODO: Float
Eq-ℕ : Eq ℕ
Eq-ℕ =
let module DecTotalOrder = Relation.Binary.DecTotalOrder in
record { decSetoid = DecTotalOrder.Eq.decSetoid ℕ.decTotalOrder }
|