bug fix

leanprover-community · May 2, 2024 · cbf357a · cbf357a
1 parent bde829b
commit cbf357a
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
@@ -386,7 +386,9 @@ def LemmaInst.matchConstInst (ci : ConstInst) (li : LemmaInst) : MetaM (HashSet
 def LemmaInst.monomorphic? (li : LemmaInst) : MetaM (Option LemmaInst) := do
   if li.params.size != 0 then
     return .none
-  let li := {li with type := ← prepReduceExpr li.type}
+  -- Do not use `prepReduceExpr` because lemmas about
+  --   recursors might be reduced to tautology
+  let li := {li with type := ← Core.betaReduce li.type}
   if !(← Expr.leadingForallQuasiMonomorphic li.type) then
     return .none
   Meta.withNewMCtxDepth do