parameters and tactics

Stream: general

[Reid Barton]

There's some issue with referring to top-level definitions which mention currently-active parameters from within a tactic block, where the parameters don't get passed automatically. I found a workaround, though--if you wrap the tactic block in let foo := foo in ... then the second foo correctly gets its automatic parameters, and inside the tactic block foo will refer to the one we just defined.

[Simon Hudon]

It is a known issue. I believe the developers intend on fixing that behavior in Lean 4.