Patterns for binder-like notations

Stream: mathlib4

[Anatole Dedecker]

How hard would it be to have pattern matching for binder-like notation like docs#iSup or docs#finsum? I want to write a sum over a triple product and I'm very sad that I have to do things like ijk.2.1. That feels so Lean3 :grinning_face_with_smiling_eyes:

[Kyle Miller]

Here's something that seems to work:

macro (priority := low) "⨆ " t:term ", " body:term:60 : term => `(iSup (fun $t => $body))

variable (f : α → β → Set γ)

#check ⨆ (p : α × β), f p.1 p.2
#check ⨆ (⟨x, y⟩ : α × β), f x y

It needs priority := low so it tries the one defined by notation3 first, otherwise you get an ambiguous interpretation error.

[Anatole Dedecker]

Thanks a lot Kyle! Could it also be made to work with multiple binders? Sorry I should try to learn these basic things at some point :sweat_smile:

[Kyle Miller]

Yeah,

macro (priority := low) "⨆ " ts:term:max* ", " body:term:60 : term => `(iSup (fun $ts* => $body))

but be warned that you can't interleave this notation with anything involving extended binders. (Probably we need to extend extBinders to support this correctly.)

[Kyle Miller]

std4#234 is a PR that's a first step to get pattern matching for notation defined by notation3. The next step would be to update https://github.com/leanprover-community/mathlib4/blob/289d4614f7ce6887b91265508ba35ff04922b9ba/Mathlib/Mathport/Notation.lean#L40-L55 with the new extBinder syntax.