Def Lean.NameMap.filter

Modification history

2024-01-05 01:23
Mathlib/Lean/Data/NameMap.lean
chore: bump std4 dependency (#9426) …
Deleted Lean.NameMap.filterView on Github →
2023-08-06 16:57
Mathlib/Lean/Data/NameMap.lean
feat(ImportGraph): add option to exclude imports from other packages (#6151) …
Added Lean.NameMap.filterView on Github →