Mercurial > hg > Members > atton > agda > systemF

comparison systemF.agda @ 18:08b8ced4e90e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lemma-R
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 10 Apr 2014 13:21:13 +0900
parents cc34bf8772a9
children 9eb6fcf6fc7d
comparison
equal deleted inserted replaced
17:cc34bf8772a9 18:08b8ced4e90e
119 119
120 -- cannot prove general Int 120 -- cannot prove general Int
121 -- 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 > 121 -- 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 >
122 -- lemma-it-n = refl 122 -- lemma-it-n = refl
123 123
124 R : {l : Level} -> {U : Set l} -> U -> (U → Int → U) -> Int -> U 124 R : {l : Level} -> {U : Set l} -> U -> (U -> Int -> U) -> Int -> U
125 R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {l} {U} {f}) t) 125 R {l} {U} u f t = π1 (It {suc l} {U × Int} < u , O > (g {_} {_} {f}) t)
126
127 lemma-R-O : {l : Level} {U : Set l} {u : U} {f : (U -> Int -> U)} -> R u f O ≡ u
128 lemma-R-O = refl
129
130 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 > ))
131 lemma-R-n = refl