We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 5dd8503 commit 1dc1269Copy full SHA for 1dc1269
2 files changed
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
@@ -440,7 +440,6 @@ scoped elab:max "d%" ppSpace t:term:arg : term => do
440
let (srcI, _tgtI) ← findModels e none
441
mkAppM ``mvfderiv #[srcI, e]
442
443
-#exit
444
open Bundle PrettyPrinter Delaborator SubExpr
445
446
/-- Delaborator for `mvfderiv`. -/
0 commit comments