Mercurial > hg > Members > atton > agda > systemF
changeset 16:93705fd8f577
Add comment to g
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 10 Apr 2014 11:30:37 +0900 (2014-04-10) |
parents | 8c735b9ebf5a |
children | cc34bf8772a9 |
files | systemF.agda |
diffstat | 1 files changed, 3 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/systemF.agda Tue Apr 08 17:18:00 2014 +0900 +++ b/systemF.agda Thu Apr 10 11:30:37 2014 +0900 @@ -117,5 +117,6 @@ g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int) g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) > -lemma-it-n : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n > -lemma-it-n = refl \ No newline at end of file +-- cannot prove general Int +-- lemma-it-n : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n > +-- lemma-it-n = refl