Notation failure for modelWithCornersEuclideanHalfSpace

Stream: mathlib4

[Michael Rothgang]

The following was minimized from #15891: removing brackets leads to a confusing error message.

import Mathlib
open scoped Manifold

instance {n : ℕ} [NeZero n] : Zero (EuclideanHalfSpace n) where
  zero :=  ⟨fun _ ↦ 0, by norm_num⟩

-- works fine
lemma modelWithCornersEuclideanHalfSpace_zero {n : ℕ} [NeZero n] : (𝓡∂ n) 0 = 0 := rfl

-- fails
/--
error: function expected at
  n
term has type
  ℕ
---
error: function expected at
  n
term has type
  ℕ
---
error: function expected at
  n
term has type
  ℕ
-/
#guard_msgs in
lemma fails {n : ℕ} [NeZero n] : 𝓡∂ n 0 = 0 := rfl

@Yaël Dillies suggested That sounds like a missing withOverApp or something like that.
Any notation experts here who can chime in? CC @Kyle Miller @Floris van Doorn

[Yaël Dillies]

I think my withOverApp is a confusion with the delaborator. Still, you should definitely be able to do notation for functions!

[Yaël Dillies]

Actually, aren't you simply missing an :args on the notation? It would be helpful to reproduce the notation here

[Michael Rothgang]

Sure, the code for the notation is

/-- The model space used to define `n`-dimensional real manifolds with boundary. -/
scoped[Manifold]
  notation3 "𝓡∂ " n =>
    (modelWithCornersEuclideanHalfSpace n :
      ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n))

[Michael Rothgang]

(in Geometry/Manifold/Instances/Real.lean)

[Yaël Dillies]

How does

/-- The model space used to define `n`-dimensional real manifolds with boundary. -/
scoped[Manifold]
  notation3 "𝓡∂ ":arg n =>
    (modelWithCornersEuclideanHalfSpace n :
      ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n))

fare? (on mobile currently, so untested)

[Eric Wieser]

I guess the question is whether 𝓡∂ f x is intended to parse as 𝓡∂ (f x) or (𝓡∂ f) x

[Michael Rothgang]

The syntax doesn't parse: unexpected token ':'; expected '=>'

[Yaël Dillies]

And what if you replace notation3 with notation?

[Michael Rothgang]

The same error. Here's the updated MWE to test

import Mathlib
open scoped Manifold

instance {n : ℕ} [NeZero n] : Zero (EuclideanHalfSpace n) where
  zero :=  ⟨fun _ ↦ 0, by norm_num⟩

/-- The model space used to define `n`-dimensional real manifolds with boundary. -/
scoped[Manifold]
  notation "foo ":arg n =>
    (modelWithCornersEuclideanHalfSpace n :
      ModelWithCorners ℝ (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace n))
-- works fine
lemma modelWithCornersEuclideanHalfSpace_zero {n : ℕ} [NeZero n] : (𝓡∂ n) 0 = 0 := rfl
-- fails
/--
error: elaboration function for 'Manifold.termFoo' has not been implemented
  foo
-/
#guard_msgs in
lemma fails {n : ℕ} [NeZero n] : foo n 0 = 0 := rfl