fix: cbv now unfolds nullary constant definitions (#12615)

This PR fixes a flipped condition in `handleConst` that prevented `cbv`
from unfolding nullary (non-function) constant definitions like
`def myVal : Nat := 42`. The check `unless eType matches .forallE` was
intended to skip bare function constants (whose unfold theorems expect
arguments) but instead skipped value constants. The fix changes the
guard to `if eType matches .forallE`, matching the logic used in the
standard `simp` ground evaluator.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -150,7 +150,8 @@ def handleConst : Simproc := fun e => do
   unless info.isDefinition do return .rfl
   let eType ← Sym.inferType e
   let eType ← whnfD eType
-  unless eType matches .forallE .. do
+  -- We don't unfold bare constants that take arguments
+  if eType matches .forallE .. then
     return .rfl
   -- TODO: Check if we need to look if we applied all the levels correctly
   let some thm ← getUnfoldTheorem n | return .rfl

tests/lean/run/cbv_nullary.lean

@@ -0,0 +1,46 @@
+set_option cbv.warning false
+
+/-! Tests for `cbv` evaluation of nullary (non-function) constants.
+
+Nullary definitions like `def myNat : Nat := 42` should be unfolded by `cbv`
+so that ground term evaluation (e.g. `evalEq`, `evalLT`) can recognize their
+values as literals.
+-/
+
+def myNat : Nat := 42
+
+-- Arithmetic: argument goes through pattern matching in Nat.add
+example : myNat + 1 = 43 := by cbv
+
+-- Direct equality
+example : myNat = 42 := by cbv
+
+-- Prop-level equality and comparisons
+example : (myNat = myNat) = True := by cbv
+example : (myNat = 42) = True := by cbv
+example : (myNat < 100) = True := by cbv
+example : (myNat ≤ 42) = True := by cbv
+
+-- Bool-level equality
+example : (myNat == 42) = true := by cbv
+
+-- Condition involving a nullary constant
+example : (if myNat = 42 then 1 else 0) = 1 := by cbv
+
+-- String nullary constant
+def myStr : String := "hello"
+
+example : myStr.length = 5 := by cbv
+example : (myStr = "hello") = True := by cbv
+
+-- Custom inductive type
+inductive Color where | red | green | blue
+
+def myColor : Color := .red
+
+def colorToNat : Color → Nat
+  | .red => 1
+  | .green => 2
+  | .blue => 3
+
+example : colorToNat myColor = 1 := by cbv