mathlib
916aaa16 - chore(*): remove default.lean files that had nothing but imports (#18408)

Commit

2 years ago

chore(*): remove default.lean files that had nothing but imports (#18408)

Author

urkud

urkud

Parents

Loading