Skip to content

Commit 2d767d6

Browse files
grunweggrunweg
committed
chore: rename fun_prop test files (#39278)
After #39261, the only remaining files are fun_prop2.lean and fun_prop_dev.lean. Rename them to something more telling, and make them UpperCamelCase while at it. (The latter is mathlib's policy for module names anyway.)
1 parent 03cc2f9 commit 2d767d6

2 files changed

File tree

MathlibTest/fun_prop2.lean renamed to MathlibTest/FunProp.lean

File renamed without changes.

MathlibTest/fun_prop_dev.lean renamed to MathlibTest/FunPropMinimal.lean

File renamed without changes.

0 commit comments

Comments
 (0)