Def Lean.NameSet.append

Modification history

2023-10-17 14:33
Mathlib/Lean/Expr/Basic.lean
Revert "chore: revert #7703 (#7710)" …
Deleted Lean.NameSet.appendView on Github →
2023-10-16 19:01
Mathlib/Lean/Expr/Basic.lean
chore: revert #7703 (#7710) …
Added Lean.NameSet.appendView on Github →
2023-10-16 04:14
Mathlib/Lean/Expr/Basic.lean
chore: bump toolchain to v4.2.0-rc2 (#7703) …
Deleted Lean.NameSet.appendView on Github →
2023-06-28 11:45
Mathlib/Lean/Expr/Basic.lean
feat: #redundant_imports / #minimize_imports commands (#5441) …
Added Lean.NameSet.appendView on Github →