Restore

Author: grunweg

Mathlib/Geometry/Manifold/Notation.lean

@@ -407,8 +407,8 @@ trying to determine `I` and `J` from the local context.
 The argument `x` can be omitted. -/
 scoped elab:max "CMDiffAt[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do
   let es ← Term.elabTerm s none
-  let ef ← ensureIsFunction <|← Term.elabTerm f none
   let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let ef ← ensureIsFunction <|← Term.elabTerm f none
   let (srcI, tgtI) ← findModels ef es
   mkAppM ``ContMDiffWithinAt #[srcI, tgtI, ne, ef, es]
 
@@ -427,17 +427,17 @@ trying to determine `I` and `J` from the local context.
 `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/
 scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do
   let es ← Term.elabTerm s none
-  let ef ← ensureIsFunction <|← Term.elabTerm f none
   let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let ef ← ensureIsFunction <|← Term.elabTerm f none
   let (srcI, tgtI) ← findModels ef es
   mkAppM ``ContMDiffOn #[srcI, tgtI, ne, ef, es]
 
 /-- `CMDiff n f` elaborates to `ContMDiff I J n f`,
 trying to determine `I` and `J` from the local context.
 `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/
 scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do
-  let e ← ensureIsFunction <|← Term.elabTerm f none
   let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let e ← ensureIsFunction <|← Term.elabTerm f none
   let (srcI, tgtI) ← findModels e none
   mkAppM ``ContMDiff #[srcI, tgtI, ne, e]
 

MathlibTest/DifferentialGeometry/Notation.lean

@@ -541,24 +541,21 @@ variable {f : M → M'} {s : Set M} {m : M}
 
 variable [IsManifold I 1 M] [IsManifold I' 1 M']
 
--- TODO: can there be better error messages when forgetting the smoothness exponent?
+-- Testing error messages when forgetting the smoothness exponent or swapping arguments.
 section error
 
 -- yields a parse error, "unexpected token '/--'; expected term"
 -- #check CMDiffAt[s] f
 
--- TODO: the old error message here was better; somehow restore it!
-/-
+/--
 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
   m
 of type
@@ -569,6 +566,14 @@ to be a function, or to be coercible to a function
 #check CMDiffAt[s] f m
 
 /--
+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
   m
 of type