Auxiliary declarations now resolve like their globals (
2f17203)
Name resolution now treats auxiliary local declarations from let rec and where like the global names they stand for, competing by longest matching prefix and winning ties. This fixes subtle dotted-name misresolutions and makes lookup semantics more consistent and faster.
Structural recursion now handles recursive match discriminants (
136fe94)
Lean now translates recursive calls that appear in match discriminants as well as in alternatives, avoiding a kernel unknown constant failure and preserving structural recursion fallback behavior under async elaboration. A regression test was added for the affected pattern.
