Mercurial > hg > Members > atton > agda > systemF
changeset 28:02926d953ef7
Retry define add-r. use R twice
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 29 Apr 2014 17:20:06 +0900 |
| parents | 7b0f2025112b |
| children | dcc57765bdef |
| files | int.agda |
| diffstat | 1 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/int.agda Mon Apr 28 11:30:09 2014 +0900 +++ b/int.agda Tue Apr 29 17:20:06 2014 +0900 @@ -43,9 +43,9 @@ add {l} {U} a b = \(x : U) -> \(y : (U -> U)) -> a (b x y) y add-r : {l : Level} {U : Set l} -> Int -> Int -> Int -add-r {l} {U} a b = R a (\x -> \n -> S x) b +add-r {l} {U} a b = R O (\x -> \_ -> S x) (R a (\x -> \_ -> S x) b) -lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {l} {U} +lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {_} {U} lemma-same-add = refl lemma-add-zero-zero : {l : Level} {U : Set l} -> add O O ≡ O {_} {U}