Skip to content

Commit 4aec2ac

Browse files
grunweggrunweg
committed
chore: move differential geometry elaborators tests into a separate directory (#35891)
1 parent 46b9dfd commit 4aec2ac

File tree

3 files changed

+0
-0
lines changed

3 files changed

+0
-0
lines changed

MathlibTest/DifferentialGeometry/NotationAdvanced.lean renamed to MathlibTest/DifferentialGeometry/Notation/Advanced.lean

File renamed without changes.

MathlibTest/DifferentialGeometry/Notation.lean renamed to MathlibTest/DifferentialGeometry/Notation/Basic.lean

File renamed without changes.

MathlibTest/DifferentialGeometry/NotationSphere.lean renamed to MathlibTest/DifferentialGeometry/Notation/Sphere.lean

File renamed without changes.

0 commit comments

Comments
 (0)