Use level in basic/list
author Yasutaka Higa Sun, 19 Oct 2014 12:22:54 +0900 169ec60fcd36 6ce83b2c9e59 agda/basic.agda agda/list.agda 2 files changed, 7 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
```--- a/agda/basic.agda	Sat Oct 18 14:22:34 2014 +0900
+++ b/agda/basic.agda	Sun Oct 19 12:22:54 2014 +0900
@@ -9,4 +9,4 @@
f ∙ g = \x -> f (g x)

postulate String : Set
-postulate show   : {A : Set} -> A -> String
\ No newline at end of file
+postulate show   : {l : Level} {A : Set l} -> A -> String
\ No newline at end of file```
```--- 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```