Mercurial > hg > Members > atton > agda > systemF
changeset 23:46fce75667cb
Retry prove lemma-list-nil-cons. but not finished.
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 15 Apr 2014 17:42:56 +0900 |
| parents | 1fbfc92d76b5 |
| children | 36d0732d28e5 |
| files | systemF.agda |
| diffstat | 1 files changed, 5 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/systemF.agda Tue Apr 15 17:20:52 2014 +0900 +++ b/systemF.agda Tue Apr 15 17:42:56 2014 +0900 @@ -161,16 +161,11 @@ 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 --- apply nil and cons to List U, return same list. but cannot justify type of cons and ListIt. --- if W = List U, cons has List U -> List (List U) -> (List U) - ---lemma-list-nil-cons : {l ll : Level} {U : Set ?} {X : Set ?} {t : List U} -> (ListIt {?} {?} {?} {List U} (nil) (cons) t) ≡ t +--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 --- try concreate variable. has yellow. +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) ---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-val : {l : Level} {U : Set l} -> (ListIt {l} {U} {suc l} {List U} (nil {l} {U}) (cons {l} {U} {l}) li) ≡ li ---lemma-list-nil-cons-val = refl \ No newline at end of file +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