Def missingInitImports

Modification history

2025-06-03 08:51

scripts/lint-style.lean

chore: bump toolchain to v4.21.0-rc1 (#25384)

Modified missingInitImports View on Github →

2025-05-19 09:39

scripts/lint-style.lean

feat(scripts/lint-style): select linters with Lakefile options (#24953) …

Modified missingInitImports View on Github →

2025-05-16 15:37

scripts/lint-style.lean

feat(lint-style): enforce modules are named in UpperCamelCase (#24654) …

Added missingInitImports View on Github →