Zulip Chat Archive

Stream: mathlib4

Topic: Shadow notation

Yaël Dillies (Jun 01 2023 at 07:08):

Why is the notation for docs4#Finset.shadow so borked? The file is littered with (∂ ) 𝒜.

Mario Carneiro (Jun 01 2023 at 07:37):

It appears to be an issue with the notation pretty printer

Mario Carneiro (Jun 01 2023 at 07:38):

actually not just the pretty printer, #check fun x => ∂ x doesn't parse

Mario Carneiro (Jun 01 2023 at 07:39):

The precedence on the notation is too low

Mario Carneiro (Jun 01 2023 at 07:39):

with notation:max "∂" => Finset.shadow it works as expected

Mario Carneiro (Jun 01 2023 at 07:39):

or just notation "∂" => Finset.shadow

Mario Carneiro (Jun 01 2023 at 07:40):

unfortunately it's too late for mathport, although I suppose you can fix it with some find/replace

Yaël Dillies (Jun 01 2023 at 08:21):

Mario Carneiro said:

or just notation "∂" => Finset.shadow

What's the default precedence?

Last updated: Dec 20 2023 at 11:08 UTC