module Eq where
open import Data.Nat
open import Data.Bool
open import Data.List

record Eq (A : Set) : Set where
  field
    _==_ : A -> A -> Bool

_==Nat_ : ℕ -> ℕ -> Bool
zero    ==Nat zero    = true
(suc n) ==Nat zero    = false
zero    ==Nat (suc m) = false
(suc n) ==Nat (suc m) = n ==Nat m


instance
  _ : Eq ℕ
  _ = record { _==_ = _==Nat_}

_||_ : Bool -> Bool -> Bool
true  || _ = true
false || x = x

elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool
elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs)
elem         x []        = false

listHas4 : Bool
listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true