Lean4
/-- Code action to create a `calc` tactic from the current goal. -/
@[tactic_code_action calcTactic]
def createCalc : TacticCodeAction := fun _params _snap ctx _stack node => do
let .node (.ofTacticInfo info) _ := node |
return #[]
if info.goalsBefore.isEmpty then
return #[]
let eager :=
{ title := s!"Generate a calc block."
kind? := "quickfix" }
let doc ← readDoc
return
#[{ eager
lazy? :=
some
(do
let tacPos := doc.meta.text.utf8PosToLspPos info.stx.getPos?.get!
let endPos := doc.meta.text.utf8PosToLspPos info.stx.getTailPos?.get!
let goal := info.goalsBefore[0]!
let goalFmt ←
ctx.runMetaM { } <|
goal.withContext do
Meta.ppExpr (← goal.getType)
return
{ eager with
edit? :=
some <|
.ofTextEdit doc.versionedIdentifier
{ range := ⟨tacPos, endPos⟩, newText := s! "calc {goalFmt} := by sorry" } }) }]
