Mercurial > hg > Members > atton > delta_monad
annotate agda/list.agda @ 26:5ba82f107a95
Define Similar in Agda
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Oct 2014 14:43:33 +0900 |
| parents | a5aadebc084d |
| children | 33b386de3f56 |
| rev | line source |
|---|---|
| 25 | 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 | |
|
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
17 [[_]] : {A : Set} -> A -> List A |
|
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
18 [[ x ]] = x :: [] |
|
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
19 |
| 25 | 20 |
| 21 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs | |
| 22 empty-append [] = refl | |
| 23 empty-append (x :: xs) = begin | |
| 24 x :: (xs ++ []) | |
| 25 ≡⟨ cong (_::_ x) (empty-append xs) ⟩ | |
| 26 x :: xs | |
| 27 ∎ |