Lean4
/-- Construct the `RewriteInterface` from a `Rewrite`. -/
def toInterface (rw : Rewrite) (name : Name ⊕ FVarId) (occ : Option Nat) (loc : Option Name) (range : Lsp.Range) :
MetaM RewriteInterface := do
let tactic ← tacticSyntax rw occ loc
let tactic ← tacticPasteString tactic range
let replacementString := Format.pretty (← ppExpr rw.replacement)
let mut extraGoals := #[]
for (mvarId, bi) in rw.extraGoals do
if bi.isExplicit then
let extraGoal ← ppExprTagged (← instantiateMVars (← mvarId.getType))
extraGoals := extraGoals.push extraGoal
match name with
| .inl name =>
let prettyLemma :=
match ← ppExprTagged (← mkConstWithLevelParams name) with
| .tag tag _ => .tag tag (.text s! "{name}")
| code => code
let lemmaType := (← getConstInfo name).type
return { rw with tactic, replacementString, extraGoals, prettyLemma, lemmaType }
| .inr fvarId =>
let prettyLemma ← ppExprTagged (.fvar fvarId)
let lemmaType ← fvarId.getType
return { rw with tactic, replacementString, extraGoals, prettyLemma, lemmaType }
