elabUnfoldCommand — Mathlib

Lean4
/-- Elaborate a `#unfold?` command. -/
@[command_elab unfoldCommand]
def elabUnfoldCommand : Command.CommandElab := fun stx =>
  withoutModifyingEnv <|
    Command.runTermElabM fun _ =>
      Term.withDeclName `_unfold do
        let e ← Term.elabTerm stx[1] none
        Term.synthesizeSyntheticMVarsNoPostponing
        let e ← Term.levelMVarToParam (← instantiateMVars e)
        let e ← instantiateMVars e
        let unfolds ← filteredUnfolds e
        if unfolds.isEmpty then
          logInfo m! "No unfolds found for {e}"
        else
          let unfolds := unfolds.toList.map (m!"· {·}")
          logInfo ((m! "Unfolds for {e}:\n") ++ .joinSep unfolds "\n")
Похожие утверждения