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)