One more test

Author: grunweg

Mathlib/Geometry/Manifold/Notation.lean

@@ -401,6 +401,9 @@ scoped elab:max "MDiff" ppSpace t:term:arg : term => do
   let (srcI, tgtI) ← findModels e none
   mkAppM ``MDifferentiable #[srcI, tgtI, e]
 
+-- We ensure the type of `n` before checking `f` is a function to provide better error messages
+-- in case e.g. just `n` was forgotten.
+
 /-- `CMDiffAt[s] n f x` elaborates to `ContMDiffWithinAt I J n f s x`,
 trying to determine `I` and `J` from the local context.
 `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).

MathlibTest/DifferentialGeometry/Notation.lean

@@ -581,11 +581,29 @@ of type
 to be a function, or to be coercible to a function
 -/
 #guard_msgs in
-#check CMDiffAt[s] f m
+#check CMDiff[s] f m
 
--- yields a parse error, "unexpected toekn '/--'; expected term"
+-- yields a parse error, "unexpected token '/--'; expected term"
 -- #check CMDiffAt f
 
+/--
+error: Type mismatch
+  f
+has type
+  M → M'
+of sort `Type (max u_10 u_4)` but is expected to have type
+  WithTop ℕ∞
+of sort `Type`
+---
+error: Expected
+  n
+of type
+  Option ℕ∞
+to be a function, or to be coercible to a function
+-/
+#guard_msgs in
+#check CMDiff f n
+
 end error
 
 /-- info: ContMDiffWithinAt I I' 1 f s : M → Prop -/