Mercurial > hg > Members > atton > agda > systemF
changeset 18:08b8ced4e90e
lemma-R
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 10 Apr 2014 13:21:13 +0900 |
| parents | cc34bf8772a9 |
| children | 9eb6fcf6fc7d |
| files | systemF.agda |
| diffstat | 1 files changed, 8 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/systemF.agda Thu Apr 10 11:34:43 2014 +0900 +++ b/systemF.agda Thu Apr 10 13:21:13 2014 +0900 @@ -121,5 +121,11 @@ -- 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 +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 {_} {_} {f}) t) + +lemma-R-O : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} -> R u f O ≡ u +lemma-R-O = refl + +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