Lean4
/-- Elaborate a `#rw??` command. -/
@[command_elab rw??Command]
def elabrw??Command : Command.CommandElab := fun stx =>
withoutModifyingEnv <|
Command.runTermElabM fun _ => do
let e ← Term.elabTerm stx[2] none
Term.synthesizeSyntheticMVarsNoPostponing
let e ← Term.levelMVarToParam (← instantiateMVars e)
let filter := stx[1].isNone
let mut rewrites := #[]
for rws in ← getModuleRewrites e do
let rws ←
if filter then
filterRewrites e rws (·.1.replacement) (·.1.makesNewMVars)
else
pure rws
rewrites := rewrites.push (rws, true)
for rws in ← getImportRewrites e do
let rws ←
if filter then
filterRewrites e rws (·.1.replacement) (·.1.makesNewMVars)
else
pure rws
rewrites := rewrites.push (rws, false)
let sections ← liftMetaM <| rewrites.filterMapM SectionToMessageData
if sections.isEmpty then
logInfo m! "No rewrites found for {e}"
else
logInfo (.joinSep sections.toList "\n\n")
