Mercurial > hg > Papers > 2018 > suruga-thesis

comparison paper/final_main/src/Eq.Agda @ 4:0f938112b48e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add paper
author suruga
date Thu, 15 Feb 2018 14:48:08 +0900
parents
children
comparison
equal deleted inserted replaced
3:8faea9c319ed 4:0f938112b48e
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