From 00178b181267c0869a38c12bc1a56218db5adda7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Nov 2024 16:17:14 -0800 Subject: [PATCH] fix: refine `Meta.Config.beta` behavior --- src/Lean/Meta/WHNF.lean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 067ab7d7bbd8..f841770ee236 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -572,7 +572,17 @@ where return (← go <| mkAppN (b.instantiate1 v) args) let f := f.getAppFn let f' ← go f - if cfg.beta && f'.isLambda then + /- + If `f'` is a lambda, then we perform beta-reduction here IF + 1- `cfg.beta` is enabled, OR + 2- `f` was not a lambda expression. That is, `f` was reduced, and the beta-reduction step is part + of this step. This is similar to allowing beta-reduction while unfolding expressions even if `cfg.beta := false`. + + We added case 2 because a failure at `norm_cast`. See test `6123_mod_cast.lean`. + Another possible fix to this test is to set `beta := true` at the `Simp.Config` value at + `NormCast.lean`. + -/ + if f'.isLambda && (cfg.beta || !f.isLambda) then let revArgs := e.getAppRevArgs go <| f'.betaRev revArgs else if let some eNew ← whnfDelayedAssigned? f' e then