Def Mathlib.Linter.DirectoryDependency.NamePrefixRel.findAny

Modification history

2025-03-31 05:22

Mathlib/Tactic/Linter/DirectoryDependency.lean

feat(Tactic/Linter): a linter for directory dependencies (#23088) …

Added Mathlib.Linter.DirectoryDependency.NamePrefixRel.findAny View on Github →