Mercurial > hg > Members > atton > agda > systemF

changeset 29:dcc57765bdef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix R arguments for check speed up
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 29 Apr 2014 17:28:26 +0900
parents 02926d953ef7
children 42027b9a70ef
files int.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/int.agda	Tue Apr 29 17:20:06 2014 +0900
+++ b/int.agda	Tue Apr 29 17:28:26 2014 +0900
@@ -42,8 +42,8 @@
 add : {l : Level} {U : Set l} -> Int -> Int -> Int
 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 O (\x -> \_ -> S x) (R a (\x -> \_ -> S x) b)
+add-r : {l : Level} {U : Set l} -> Int -> Int -> Int {{!!}} {{!!}}
+add-r {l} {U} a b = (R (R O (\x -> \_ -> S x) a) (\x -> \_ -> S x) b)
 
 lemma-same-add : {l : Level} {U : Set l} -> add ≡ add-r {_} {U}
 lemma-same-add = refl