Mercurial > hg > Members > atton > delta_monad

annotate agda/list.agda @ 58:1229ee398567

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mini fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 22 Nov 2014 12:34:06 +0900
parents 743c05b98dad
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module list where
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
37
743c05b98dad Use level in basic/list
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
3 open import Level
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Relation.Binary.PropositionalEquality
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open ≡-Reasoning
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 infixr 40 _::_
37
743c05b98dad Use level in basic/list
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
8 data List {l : Level} (A : Set l) : (Set l)where
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 [] : List A
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 _::_ : A -> List A -> List A
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 infixl 30 _++_
37
743c05b98dad Use level in basic/list
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
14 _++_ : {l : Level} {A : Set l} -> List A -> List A -> List A
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 [] ++ ys = ys
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 (x :: xs) ++ ys = x :: (xs ++ ys)
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
37
743c05b98dad Use level in basic/list
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
18 [[_]] : {l : Level} {A : Set l} -> A -> List A
26
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 25
diff changeset
19 [[ x ]] = x :: []
5ba82f107a95 Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 25
diff changeset
20
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
37
743c05b98dad Use level in basic/list
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
22 empty-append : {l : Level} {A : Set l} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs
25
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 empty-append [] = refl
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 empty-append (x :: xs) = begin
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 x :: (xs ++ [])
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 ≡⟨ cong (_::_ x) (empty-append xs) ⟩
a5aadebc084d Define List in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 x :: xs
31
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
28 ∎
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
29
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
30
37
743c05b98dad Use level in basic/list
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 31
diff changeset
31 list-associative : {l : Level} {A : Set l} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c)
31
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
32 list-associative [] b c = refl
33b386de3f56 Proof list-associative
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
33 list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c)