From c83f5d8201362b26a749138f6dbff2dd509f85b1 Mon Sep 17 00:00:00 2001 From: Harley Eades Date: Sun, 9 Apr 2017 10:26:57 -0400 Subject: [PATCH] Fixed a bug when translating copy. New example: ILL> :t \x:!A.copy x as z,y in z (x) y !A -o (!A (x) !A) --- Source/ALL/Languages/ILL/AgdaInterface.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/ALL/Languages/ILL/AgdaInterface.agda b/Source/ALL/Languages/ILL/AgdaInterface.agda index 1e293fb..2887a81 100644 --- a/Source/ALL/Languages/ILL/AgdaInterface.agda +++ b/Source/ALL/Languages/ILL/AgdaInterface.agda @@ -44,7 +44,7 @@ translate (Promote ts t) = translate (Copy t₁ x y t₂) = (translate t₁) >>=E (λ tt₁ → (translate t₂) >>=E - (λ tt₂ → Right (close-t 0 x LCPV x (close-t 0 y RCPV y tt₂)))) + (λ tt₂ → right (Copy tt₁ (x , y) (close-t 0 x LCPV x (close-t 0 y RCPV y tt₂))))) translate (Discard t₁ t₂) = (translate t₁) >>=E (λ tt₁ → translate t₂ >>=E