scoped[NS]

Stream: mathlib4

[Jireh Loreaux]

I tried to use the scoped[namespace] syntax for localized notation but I got the error: elaboration function for 'Mathlib.Tactic.scopedNS' has not been implemented @Mario Carneiro

[Mario Carneiro]

did you import Mathlib.Tactic.ScopedNS? It works for me in a basic test

[Jireh Loreaux]

yeah, I did. I'll play around and ask again tomorrow with a #mwe if it's still broken.

[Jireh Loreaux]

I think the problem is the notation I was trying to declare was infixl:

import Mathlib.Tactic.ScopedNS

def Foo : ℕ → ℕ := id

-- scoped[Bar] infixl:40 " ⟹ " => Foo -- fails
scoped[Bar] notation " ⟹ " => Foo -- succeeds

[Jireh Loreaux]

I understand. I guess it just needs another macro rule. I'll try to add it.

[Jireh Loreaux]

Oh, actually, it looks to me like it should be supported by the second rule. :thinking: And the docstring says it should support infix.

[Jireh Loreaux]

The type on $mixfixKind:prefix looks wrong. I thought it should be $mixfixKind:mixfix, but that doesn't work.

[Mario Carneiro]

yeah, the notation wasn't designed in a way that facilitates matching on it

[Mario Carneiro]

mathlib4#676

[Jireh Loreaux]

Now infixl works but notation is broken (same error as before):

import Mathlib.Tactic.ScopedNS

def Foo : ℕ → ℕ := id

scoped[Bar] infixl:40 " ⟹ " => Foo -- succeeds
scoped[Bar] notation " ⟹ " => Foo -- fails

[Jireh Loreaux]

I think it's just that the precedence changed from being optional to mandatory. I'll push a fix. (Note: it works if you include the precedence.)

[Jireh Loreaux]

Or is the mandatory precedence intentional?

[Mario Carneiro]

I pushed a fix

[Jireh Loreaux]

Thanks. You beat me to it, I had just made the PR.

[Mario Carneiro]

I also added support for doc comments and attributes

[Jireh Loreaux]

Nice, thanks!

[Winston Yin]

The scoped notation [a, b] for Set.interval a b doesn't work in mathlib4#1062. Lean4 thinks it's still a List. Any clue how to fix it?

[Mario Carneiro]

does that notation work "normally", without scopes?

[Mario Carneiro]

I expect it to be just as dreadfully ambiguous as it always has been

[Kevin Buzzard]

It's not ambiguous if you're a mathematician and are considering what the type is. Is that asking too much of lean?

[Mario Carneiro]

no, lean supports this kind of thing in principle, I've just never found choice nodes to be reliable

[Mario Carneiro]

since you quite often have these expressions in a context with no expected type

[Winston Yin]

Removing the scope gives

ambiguous, possible interpretations
  [↑toDual a, ↑toDual b] : Set ((fun x ↦ αᵒᵈ) a)

  [↑toDual a, ↑toDual b] : List ((fun x ↦ αᵒᵈ) a)

[Mario Carneiro]

wait, so what does working look like?

[Winston Yin]

In mathlib4#1062 I temporarily removed scoped and used [[a, b]] instead of [a, b]