Mercurial > hg > Members > kono > Proof > category

changeset 329:c4514e0cf0e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no yellow on append example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Mar 2014 09:31:46 +0700
parents d6eb3520ccf8
children fa018eb1723e
files system-f.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/system-f.agda	Sat Mar 22 09:28:33 2014 +0700
+++ b/system-f.agda	Sat Mar 22 09:31:46 2014 +0700
@@ -206,7 +206,7 @@
 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 = \s t -> x (y s t) t
 
-lemma18 : Append l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
+lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {l} {Int {l} {U}} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
 Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X