From 17a4e9406376ec51434f3f29d36f53f0fa2dbbc7 Mon Sep 17 00:00:00 2001
From: IndPrinciple <syxx2013050321@163.com>
Date: Thu, 2 May 2024 19:22:42 +0800
Subject: [PATCH] bug fix

---
 Auto/Translation/Monomorphization.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
index 45ade29..7d41af4 100644
--- a/Auto/Translation/Monomorphization.lean
+++ b/Auto/Translation/Monomorphization.lean
@@ -783,7 +783,7 @@ namespace FVarRep
     let .sort bodylvl := bodysort
       | throwError "replacePolyWithFVar :: Unexpected error"
     let bodyrep ← replacePolyWithFVar body'
-    let .inl bodyrep ← replacePolyWithFVar body'
+    let .inl bodyrep := bodyrep
       | return bodyrep
     -- Type of type of bound variable is `Prop`
     -- Requirement: Type of body is `Prop`, and the bound variable