Why is this notation not printed

Stream: lean4

[Nir Paz]

I defined a notation and want it to show up in the infoview instead of its definition. Looking at the definitions of notations that do show up in the infoview, like ∈, I don't see a difference from mine. What makes this happen?

import Mathlib

open Set

variable {α β : Type*} {f g : α → β} {X : Set α}

notation:50 f:50 "~"X:max g:50 => (EqOn f g X)

example : f ~X g := by
  sorry -- ⊢ EqOn f g X instead of ⊢ f ~X g

[Daniel Weber]

It is because of the parenthesis around EqOn f g X - if you remove them it works (almost, you should do notation:50 f:50 " ~"X:max g:50 => EqOn f g X)

[Nir Paz]

Huh, thanks. Do you know why this happens?

[Daniel Weber]

I'd guess whatever mechanism is responsible for creating a delaborator for the notation doesn't figure out the head function correctly, but I'm not sure why

[Nir Paz]

If the definition is slightly more complicated, like
notation:50 f:50 " ~"X:max g:50 => EqOn f g X ∧ False
then it breaks again.

[Daniel Weber]

notation3 works there, I don't know why notation doesn't

[Nir Paz]

Good enough for me! But if someone can explain the difference that's causing this.

[Daniel Weber]

notation:50 f:50 " ~"X:max g:50 => And (EqOn f g X) False also works

[Daniel Weber]

docs#Lean.Elab.Command.mkUnexpander says:

Try to derive an unexpander from a notation. The notation must be of the form notation ... => c body where c is a declaration in the current scope and body any syntax that contains each variable from the LHS at most once.

[Nir Paz]

That explains it, but it seems very finicky compared to lean3.

[Eric Wieser]

Hence the 3 in notation3

[Mario Carneiro]

the reason this is so finicky is because it doesn't have type information, so it can't properly elaborate the syntax and in many cases it has to make guesses about what constants you are talking about

[Mario Carneiro]

so the current limitation is that you basically have to write it out as just nested constant applications without notation