Mercurial > hg > Members > atton > agda > systemF

changeset 19:9eb6fcf6fc7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add comments
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 10 Apr 2014 13:25:48 +0900
parents 08b8ced4e90e
children de9e05b25acf
files systemF.agda
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/systemF.agda	Thu Apr 10 13:21:13 2014 +0900
+++ b/systemF.agda	Thu Apr 10 13:25:48 2014 +0900
@@ -129,3 +129,11 @@
 
 lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) (n < u , O > (g {l} {U} {f}) (\u n ->  π2 < u , n > ))
 lemma-R-n = refl
+
+-- Proofs And Types Style lemma-R-n
+-- lemma-R-n : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} {n : Int} -> R u f (S n) ≡ f (R u f n) n
+-- n in (S n) and (R u f n) has (U × Int), but last n has Int.
+-- regenerate same (n : Int) by used g, <_,_>
+
+
+