Commit 2025-01-30 09:06 9571e4ae

feat: let notation3 pretty print "overapplied" notations (#21239) This PR makes notation3s delaborators be able to handle "overapplied" functions — these are notations that expand to functions that might then be applied to arguments. The fundamental issue is that we need to know the arity of a function to be able to keep track of how many arguments are supposed to be matched for the notation and how many are supposed to be put toward normal app delaboration. With some changes to core in the last year, we now have a withOverApp combinator we can take advantage of. To make use of it, the notation3 delaborator generator has been modified to compute arities while creating matchers. The effect is that we now observe

import Mathlib.Algebra.BigOperators.Finprod
variable (ι R : Type) (f : ι → R) [DecidableEq ι] [CommRing R]
example : (∑ᶠ (i : ι), Pi.single i (f i)) = f := by
  -- ⊢ ∑ᶠ (i : ι), Pi.single i (f i) = f
  ext j
  -- ⊢ (∑ᶠ (i : ι), Pi.single i (f i)) j = f j
  sorry

where before this PR the state after ext j was ⊢ finsum (fun i => Pi.single i (f i)) j = f j. Implementation note: matchers can be associated to multiple delaboration keys. Previously we would define a single delaborator and then give it multiple delab attributes per key. This is very rare to have more than one key. For simplicity, we now define a separate delaborator per key, since each can have its own arity processing.