Commit 2021-05-19 15:46 e5cd871f

View on Github →

feat(Tactic/OpenPrivate): allow specifying module name

Estimated changes

Modified Mathlib/Tactic/OpenPrivate.lean

modified def Lean.Elab.Command.elabOpenPrivateLike

added def Lean.Environment.declsInModuleIdx

added def Lean.Environment.moduleIdxForModule?