Commit 2023-06-02 12:48 329fc545

feat: notation3 delaborator generation (#4533) Gives the notation3 command the ability to generate a delaborator in most common situations. When it succeeds, notation3-defined syntax is pretty printable. Examples:

(⋃ (i : ι) (i' : ι'), s i i') = ⋃ (i' : ι') (i : ι), s i i'
(⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ