Beta-reduce, to not confuse delta?

leanprover · Dec 11, 2024 · 5382395 · 5382395
1 parent f9b44aa
commit 5382395
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
@@ -198,7 +198,7 @@ return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)
 -/
 private partial def curry (varNames : Array Name) (e : Expr) : MetaM Expr := do
   if varNames.isEmpty then
-    return .app e (mkConst ``Unit.unit)
+    return e.beta #[mkConst ``Unit.unit]
   let type ← whnfForall (← inferType e)
   unless type.isForall do
     throwError "curryPSigma: expected forall type, got {type}"