Mercurial > hg > Members > atton > agda > systemF

changeset 24:36d0732d28e5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add comment for lemma-list-nil-cons
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 16 Apr 2014 16:26:25 +0900
parents 46fce75667cb
children 2efb882e120d
files systemF.agda
diffstat 1 files changed, 9 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/systemF.agda	Tue Apr 15 17:42:56 2014 +0900
+++ b/systemF.agda	Wed Apr 16 16:26:25 2014 +0900
@@ -161,11 +161,16 @@
 lemma-list-it-cons : {l : Level} {U W : Set l} {u : U} {w : W} {f : U -> W -> W} {t : List U} -> ListIt w f (cons u t) ≡ f u (ListIt w f t)
 lemma-list-it-cons = refl
 
+-- cannot proove gerenal list ...?
+
 --lemma-list-nil-cons : {l ll : Level} {U : Set l} {t : List {l} {ll} U} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) t) ≡ t
 --lemma-list-nil-cons = refl
 
-li : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
-li {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil) 
+
+-- lemma-list-nil-cons for concrete list. has yellow.
 
-lemma-list-nil-cons-val : {l ll : Level} {U : Set l} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) li) ≡ li 
-lemma-list-nil-cons-val = refl
\ No newline at end of file
+--elem2-list : {l ll : Level} {U : Set l} {u1 u2 : U} -> List {l} {ll} U
+--elem2-list {l} {ll} {U} {u1} {u2} = cons u1 (cons u2 nil)
+
+--lemma-list-nil-cons-val : {l ll : Level} {U : Set l} -> (ListIt {l} {U} {(l ⊔ (suc ll))} {List {l} {ll} U} (nil {l} {U} {ll}) (cons {l} {U} {ll}) elem2-list) ≡ elem2-list
+--lemma-list-nil-cons-val = refl
\ No newline at end of file