Factorial notation parse error

Stream: mathlib4

[Floris van Doorn]

In some cases the Nat.factorial notation parses incorrectly.

import Mathlib.Data.Nat.Factorial.Basic

open Nat

example (n : ℕ) (hn : 0 < n) : n ∣ n ! := by -- fine
  have : n ∣ n ! := -- fine
    dvd_factorial hn le_rfl
  have : n ∣ n ! -- parsed incorrectly
  · exact dvd_factorial hn le_rfl
  exact dvd_factorial hn le_rfl

[Floris van Doorn]

My guess is that the · is parsed as the anonymous variable, because we're still resolving the overloaded notation ! (either not or Nat.factorial)

[Mario Carneiro]

Removing the whitespace works, since it prevents it from being treated as an application of n to ! ·. Of course the lexer issues with n! still apply, but you can write (n)! instead

[Kyle Miller]

There's also using an explicit semicolon (have : n ∣ n !;) or using parentheses around other parts of the expression (like have : n ∣ (n !)).

[Mario Carneiro]

or even (have : n ∣ n !)

[Kyle Miller]

(Javascript also has optional semicolons, and the risk of unexpected parses like this pushed me towards always using semicolons there.)

[Kyle Miller]

It's too bad that · for focusing is also a valid notation in expressions; if focusing used a unique symbol this could be less of an issue.

[Ruben Van de Velde]

Does it work if you use . (period) instead of ·?

[Mario Carneiro]

nope, . works as an ascii replacement for · in both cases

[Reid Barton]

This also wouldn't be an issue if indentation-based syntax worked like in Haskell (as discussed elsewhere)

[Johan Commelin]

Sorry for necrobumping this... I think @Kyle Miller had a parser "hack" that made factorial notation work nicely. Maybe we actually want to have that in mathlib

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20.60propose.60.20tactic/near/351149815
(it's in a propose thread since Johan came across n! not being n ! when creating a propose demo)

[Eric Wieser]

I'll note in this thread that the factorial notation is causing me trouble in #mathlib4 > Clash with factorial and EuclideanSpace notation @ 💬

[Eric Wieser]

I ran into this again with

import Mathlib

open scoped Nat

theorem fails (n : ℕ) : True := by
  let x := n !
  sorry

Is there a precedence fix here by making tactic newlines take precedence over !, like they already do over function application?

[Snir Broshi]

This works:

import Mathlib

open scoped Nat

theorem fails (n : ℕ) : True := by
  let x := (n)!
  sorry

and it's the recommended notation: https://github.com/leanprover-community/mathlib4/blob/ae97c1b7752a7c09092be88c91a75a3dd7f29ced/Mathlib/Data/Nat/Factorial/Basic.lean#L40