Documentation

Lean.Meta.Tactic.ExposeNames

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
    Instances For
      def Lean.Meta.withExposedNames {α : Type} (k : MetaM α) :

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

      Equations
        Instances For