Commit 2021-05-10 10:20 71241b35

View on Github →

feat(Tactic/OpenPrivate): Add open private command

Estimated changes

Created Mathlib/Tactic/OpenPrivate.lean

added def Lean.Elab.Command.elabExportPrivate

added def Lean.Elab.Command.elabOpenPrivate

added def Lean.Elab.Command.elabOpenPrivateLike

added def Lean.Meta.collectPrivateIn

Modified Mathlib/Tactic/Split.lean