Mercurial > hg > Members > atton > delta_monad
diff 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 |
line wrap: on
line diff
--- a/agda/list.agda Sat Oct 18 14:22:34 2014 +0900 +++ b/agda/list.agda Sun Oct 19 12:22:54 2014 +0900 @@ -1,24 +1,25 @@ module list where +open import Level open import Relation.Binary.PropositionalEquality open ≡-Reasoning infixr 40 _::_ -data List (A : Set) : Set where +data List {l : Level} (A : Set l) : (Set l)where [] : List A _::_ : A -> List A -> List A infixl 30 _++_ -_++_ : {A : Set} -> List A -> List A -> List A +_++_ : {l : Level} {A : Set l} -> List A -> List A -> List A [] ++ ys = ys (x :: xs) ++ ys = x :: (xs ++ ys) -[[_]] : {A : Set} -> A -> List A +[[_]] : {l : Level} {A : Set l} -> A -> List A [[ x ]] = x :: [] -empty-append : {A : Set} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs +empty-append : {l : Level} {A : Set l} -> (xs : List A) -> xs ++ [] ≡ [] ++ xs empty-append [] = refl empty-append (x :: xs) = begin x :: (xs ++ []) @@ -27,6 +28,6 @@ ∎ -list-associative : {A : Set} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c) +list-associative : {l : Level} {A : Set l} -> (a b c : List A) -> (a ++ (b ++ c)) ≡ ((a ++ b) ++ c) list-associative [] b c = refl list-associative (x :: a) b c = cong (_::_ x) (list-associative a b c) \ No newline at end of file