Clash with factorial and EuclideanSpace notation

Stream: mathlib4

[Eric Wieser]

What's the fix to this clash between docs#PiLp.vecNotation and docs#Nat.term_! ?

import Mathlib

#check Eq ![1, 2, 3] ![1, 2, 3] -- ok
#check Eq !₂[1, 2, 3] !₂[1, 2, 3] -- ok

open scoped Nat
#check Eq ![1, 2, 3] ![1, 2, 3] -- ok
#check Eq !₂[1, 2, 3] !₂[1, 2, 3] -- fails

(using Eq just as it's a two-argument function)

[Andrew Yang]

Does this actually happen in practice?

[Andrew Yang]

Ah probably it does and my question should be "Does this still happen in practice if the EuclideanSpace notation is scoped?"

[Eric Wieser]

I'd prefer it be possible to use both these notations without any ambiguity

[Eric Wieser]

There's no scenario in which we want n !m to parse as Nat.factorial n m

[Andrew Yang]

docs#Lean.Parser.lookahead should be useful?

[Eric Wieser]

I'm not sure how

[Eric Wieser]

Here's a mwe that includes the conflicting notations

import Mathlib.Analysis.Normed.Lp.PiLp
import Mathlib.Util.Superscript

open Lean Meta Elab Term Macro TSyntax PrettyPrinter.Delaborator SubExpr
open Mathlib.Tactic (subscriptTerm)

/-- Notation for vectors in Lp space. `!₂[x, y, ...]` is a shorthand for
`(WithLp.equiv 2 _ _).symm ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.

This also works for other subscripts. -/
syntax (name := PiLp.vecNotation) "!" noWs subscriptTerm noWs "[" term,* "]" : term
macro_rules | `(!$p:subscript[$e:term,*]) => do
  -- override the `Fin n.succ` to a literal
  let n := e.getElems.size
  `((WithLp.equiv $p <| ∀ _ : Fin $(quote n), _).symm ![$e,*])

notation:10000 n "!" => Nat.factorial n

#check Eq ![1, 2, 3] ![1, 2, 3]

#check Eq !₂[1, 2, 3] (!₂[1, 2, 3])
#check Eq !₂[1, 2, 3] !₂[1, 2, 3]

[Andrew Yang]

e.g. changing the notation to this works

syntax:10000 term atomic("!" notFollowedBy("₂")) : term
macro_rules | `($n:term !) => do `(Nat.factorial $n)

[Aaron Liu]

But then of course it breaks again on !₁[1, 2, 3]

[Andrew Yang]

Yeah. Hence the e.g.. I'm just saying that this method works but someone needs to decide what is allowed after n! and put it there.