fix leadingForallQuasiMonomorphic bug

leanprover-community · Oct 17, 2024 · 90199ee · 90199ee
1 parent 7c02984
commit 90199ee
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
@@ -440,7 +440,7 @@ where
         match ty with
         | .forallE _ _ body _ => !body.hasLooseBVar 0
         | _ => false
-      if hol && (← getMode) == .hol then
+      if hol && (← getMode) == .fol then
         return false
       let fvarSet := HashSet.empty.insertMany fvars
       if ty.hasAnyFVar fvarSet.contains then