Mercurial > hg > Members > atton > delta_monad

comparison agda/list.agda @ 25:a5aadebc084d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define List in Agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 07 Oct 2014 10:38:57 +0900
parents
children 5ba82f107a95
comparison
equal deleted inserted replaced
24:ae41becf41db 25:a5aadebc084d
1 module list where
2
3 open import Relation.Binary.PropositionalEquality
4 open ≡-Reasoning
5
6 infixr 40 _::_
7 data List (A : Set) : Set where
8 [] : List A
9 _::_ : A -> List A -> List A
10
11
12 infixl 30 _++_
13 _++_ : {A : Set} -> List A -> List A -> List A
14 [] ++ ys = ys
15 (x :: xs) ++ ys = x :: (xs ++ ys)
16
17
18 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs
19 empty-append [] = refl
20 empty-append (x :: xs) = begin
21 x :: (xs ++ [])
22 ≡⟨ cong (_::_ x) (empty-append xs) ⟩
23 x :: xs
24 ∎