Mercurial > hg > Papers > 2019 > oshiro-thesis

comparison final_pre/src/Eq.Agda @ 7:0e8b9646d43f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author e155702
date Sun, 17 Feb 2019 05:39:59 +0900
parents
children
comparison
equal deleted inserted replaced
6:8f5d263c219b 7:0e8b9646d43f
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