Skip to content

Commit c3f2e7b

Browse files
committed
Non-module version kind of works!
1 parent 6c2c410 commit c3f2e7b

2 files changed

Lines changed: 447 additions & 1 deletion

File tree

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -440,7 +440,6 @@ scoped elab:max "d%" ppSpace t:term:arg : term => do
440440
let (srcI, _tgtI) ← findModels e none
441441
mkAppM ``mvfderiv #[srcI, e]
442442

443-
#exit
444443
open Bundle PrettyPrinter Delaborator SubExpr
445444

446445
/-- Delaborator for `mvfderiv`. -/

0 commit comments

Comments
 (0)