# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1398760106 -32400
# Node ID dcc57765bdefec2c08f2df9459ebdbfcaf0c81cb
# Parent  02926d953ef711c4a7b1f439a3b1908a8311d4c9
Fix R arguments for check speed up

diff -r 02926d953ef7 -r dcc57765bdef int.agda
--- 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