Def Lean.Meta.collectPrivateIn

Modification history

2022-09-04 16:26

Mathlib/Tactic/OpenPrivate.lean

feat: depend on std4 (#397)

Deleted Lean.Meta.collectPrivateIn View on Github →

2021-05-10 10:20

Mathlib/Tactic/OpenPrivate.lean

feat(Tactic/OpenPrivate): Add `open private` command

Added Lean.Meta.collectPrivateIn View on Github →