Mercurial > hg > Members > kono > Proof > category
changeset 335:45130bd669ca
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 22 Mar 2014 18:46:51 +0700 |
parents | 357d3114c9b5 |
children | bda408a05c24 |
files | system-f.agda |
diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/system-f.agda Sat Mar 22 18:34:13 2014 +0700 +++ b/system-f.agda Sat Mar 22 18:46:51 2014 +0700 @@ -157,7 +157,7 @@ -- lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int -> U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t -- lemma17 u v t = refl --- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int -> U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t +-- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X -> U ) -> (t : Int X ) -> R u v (S t) ≡ v ( R u v t ) t List : {l : Level} (U X : Set l) -> Set l List {l} = \( U X : Set l) -> X -> ( U -> X -> X ) -> X @@ -186,13 +186,13 @@ Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List U (Bool X) -> Bool _ Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) list -Append : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X -> List U _ +Append : {l : Level} {U : Set l} {X : Set l} -> List U X -> List U X -> List U X Append x y = \s t -> x (y s t) t lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) lemma18 = refl -Reverse : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X +Reverse : {l : Level} {U : Set l} {X : Set l} -> List U (List U X) -> List U X Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( \u w -> Append w (Cons u Nil) ) x lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))