def Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId

Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name. If no local declarations require renaming, the original goal is returned unchanged.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.withExposedNames {α : Type} (k : MetaM α) : MetaM α

Creates a temporary local context where all names are exposed, and executes k

Equations

• One or more equations did not get rendered due to their size.