|
52
|
1 module Eq where
|
|
|
2 open import Data.Nat
|
|
|
3 open import Data.Bool
|
|
|
4 open import Data.List
|
|
|
5
|
|
|
6 record Eq (A : Set) : Set where
|
|
|
7 field
|
|
|
8 _==_ : A -> A -> Bool
|
|
|
9
|
|
|
10 _==Nat_ : ℕ -> ℕ -> Bool
|
|
|
11 zero ==Nat zero = true
|
|
|
12 (suc n) ==Nat zero = false
|
|
|
13 zero ==Nat (suc m) = false
|
|
|
14 (suc n) ==Nat (suc m) = n ==Nat m
|
|
|
15
|
|
|
16
|
|
|
17 instance
|
|
|
18 _ : Eq ℕ
|
|
|
19 _ = record { _==_ = _==Nat_}
|
|
|
20
|
|
|
21 _||_ : Bool -> Bool -> Bool
|
|
|
22 true || _ = true
|
|
|
23 false || x = x
|
|
|
24
|
|
|
25 elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
|
|
|
26 elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs)
|
|
|
27 elem x [] = false
|
|
|
28
|
|
|
29 listHas4 : Bool
|
|
|
30 listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true
|
