Mercurial > hg > Members > atton > agda > systemF

changeset 17:cc34bf8772a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define R
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 10 Apr 2014 11:34:43 +0900
parents 93705fd8f577
children 08b8ced4e90e
files systemF.agda
diffstat 1 files changed, 3 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/systemF.agda	Thu Apr 10 11:30:37 2014 +0900
+++ b/systemF.agda	Thu Apr 10 11:34:43 2014 +0900
@@ -120,3 +120,6 @@
 -- 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
+
+R : {l : Level} -> {U : Set l} -> U -> (U → Int → U) -> Int -> U
+R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {l} {U} {f}) t)
\ No newline at end of file