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)
heades · Apr 9, 2017 · c83f5d8 · c83f5d8
1 parent 539ef17
commit c83f5d8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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