MinImports
📁 Source: Mathlib/Tactic/MinImports.lean
Statistics
| Metric | Count |
|---|---|
| 14 | |
| Theorems | 0 |
| Total | 14 |
Mathlib.Command.MinImports
Definitions
| Name | Category | Theorems |
|---|---|---|
getAllDependencies 📖 | CompOp | — |
getAllImports 📖 | CompOp | — |
getAttrNames 📖 | CompOp | — |
getAttrs 📖 | CompOp | — |
getDeclName 📖 | CompOp | — |
getId 📖 | CompOp | — |
getIds 📖 | CompOp | — |
getIrredundantImports 📖 | CompOp | — |
getSyntaxNodeKinds 📖 | CompOp | — |
getVisited 📖 | CompOp | — |
minImpsCore 📖 | CompOp | — |
minImpsStx 📖 | CompOp | — |
previousInstName 📖 | CompOp | — |
«command#min_importsIn_» 📖 | CompOp | — |
---