type annotation still visible in context of where-bound function #11025
Description
While #9674 was effective for top-level recursive functions, it did not seem to apply to local recursive functions in where:
set_option linter.unusedVariables false
/--
trace: n✝ : Nat
x : Bool
n : Nat
⊢ Nat
-/
#guard_msgs in
def foo (n : Nat) (x := true) := match n with
| 0 => 0
| n+1 => by trace_state; exact foo n + 1
/--
trace: n✝ : Nat
x : optParam Bool true
n : Nat
⊢ Nat
-/
#guard_msgs in
def bar := go 1000
where
go (n : Nat) (x := true) := match n with
| 0 => 0
| n+1 => by trace_state; exact go n + 1
Versions
Lean 4.25.0-rc2
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.