Mercurial > hg > Members > atton > delta_monad
comparison agda/list.agda @ 37:743c05b98dad
Use level in basic/list
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 19 Oct 2014 12:22:54 +0900 |
parents | 33b386de3f56 |
children |
comparison
equal
deleted
inserted
replaced
36:169ec60fcd36 | 37:743c05b98dad |
---|---|
1 module list where | 1 module list where |
2 | 2 |
3 open import Level | |
3 open import Relation.Binary.PropositionalEquality | 4 open import Relation.Binary.PropositionalEquality |
4 open ≡-Reasoning | 5 open ≡-Reasoning |
5 | 6 |
6 infixr 40 _::_ | 7 infixr 40 _::_ |
7 data List (A : Set) : Set where | 8 data List {l : Level} (A : Set l) : (Set l)where |
8 [] : List A | 9 [] : List A |
9 _::_ : A -> List A -> List A | 10 _::_ : A -> List A -> List A |
10 | 11 |
11 | 12 |
12 infixl 30 _++_ | 13 infixl 30 _++_ |
13 _++_ : {A : Set} -> List A -> List A -> List A | 14 _++_ : {l : Level} {A : Set l} -> List A -> List A -> List A |
14 [] ++ ys = ys | 15 [] ++ ys = ys |
15 (x :: xs) ++ ys = x :: (xs ++ ys) | 16 (x :: xs) ++ ys = x :: (xs ++ ys) |
16 | 17 |
17 [[_]] : {A : Set} -> A -> List A | 18 [[_]] : {l : Level} {A : Set l} -> A -> List A |
18 [[ x ]] = x :: [] | 19 [[ x ]] = x :: [] |
19 | 20 |
20 | 21 |
21 empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs | 22 empty-append : {l : Level} {A : Set l} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs |
22 empty-append [] = refl | 23 empty-append [] = refl |
23 empty-append (x :: xs) = begin | 24 empty-append (x :: xs) = begin |
24 x :: (xs ++ []) | 25 x :: (xs ++ []) |
25 ≡⟨ cong (_::_ x) (empty-append xs) ⟩ | 26 ≡⟨ cong (_::_ x) (empty-append xs) ⟩ |
26 x :: xs | 27 x :: xs |
27 ∎ | 28 ∎ |
28 | 29 |
29 | 30 |
30 list-associative : {A : Set} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c) | 31 list-associative : {l : Level} {A : Set l} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c) |
31 list-associative [] b c = refl | 32 list-associative [] b c = refl |
32 list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c) | 33 list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c) |