bug fix

leanprover-community · May 2, 2024 · 17a4e94 · 17a4e94
1 parent 74a99bc
commit 17a4e94
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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