Mercurial > hg > Members > kono > Proof > category
changeset 328:d6eb3520ccf8
Append
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Mar 2014 09:28:33 +0700 |
| parents | 7645185970f2 |
| children | c4514e0cf0e2 |
| files | system-f.agda |
| diffstat | 1 files changed, 6 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/system-f.agda Sat Mar 22 08:53:02 2014 +0700 +++ b/system-f.agda Sat Mar 22 09:28:33 2014 +0700 @@ -188,13 +188,13 @@ Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List {l} {U} {X} -> List {l} {U} {X} Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y ) -l0 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X} +l0 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'} l0 = Nil -l1 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X} +l1 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'} l1 = Cons n1 Nil -l2 : {l : Level} {X : Set l} -> List {l} {Int {l} {X}} {X} +l2 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'} l2 = Cons n2 l1 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W @@ -204,10 +204,10 @@ Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool} {X} T (\u w -> F) list Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_} -Append {l} {U} {X} x y = ListIt {l} {U} {_} {X} y (\u w -> Cons u w) x +Append {l} {U} {X} x y = \s t -> x (y s t) t --- lemma18 : Append l1 l2 ≡ Cons n1 ( Cons n2 Nil ) --- lemma18 = refl +lemma18 : Append l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) +lemma18 = refl Tree = \{l : Level} -> \{ U X : Set l} -> X -> ( (U -> X) -> X ) -> X