Can't refer to anonymous match in section with parameters

[digama0]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

A short code section with the issue:

section
parameter α : Type
include α

def foo : nat := match 0 with _ := 0 end

example : nat := foo._match_1 ()
end

The foo._match_1 reference is interpreted as a field access, even though one can verify that foo._match_1 is the exact name of the anonymous match. Presumably this is due to some shadowing of the foo symbol by the local notation foo caused by the parameter. Are there any suggested workarounds?

[leodemoura]

Are there any suggested workarounds?

Use @foo._match_1

full example:

section
parameter α : Type
include α

def foo : nat := match 0 with _ := 0 end

example : nat := @foo._match_1 0
end