Miscellaneous code actions

This declares some basic tactic code actions, using the @[tactic_code_action] API.

def Std.CodeAction.findStack? (root : Lean.Syntax) (target : Lean.Syntax) : Option Lean.Syntax.Stack

Return the syntax stack leading to target from root, if one exists.

def Std.CodeAction.holeKindToHoleString (elaborator : Lean.Name) (synthName : String) : String

Constructs a hole with a kind matching the provided hole elaborator.

def Std.CodeAction.instanceStub : Std.CodeAction.HoleCodeAction

Hole code action used to fill in a structure's field when specifying an instance.

In the following:

instance : Monad Id := _

invoking the hole code action "Generate a skeleton for the structure under construction." produces:

instance : Monad Id := {
  map := _
  mapConst := _
  pure := _
  seq := _
  seqLeft := _
  seqRight := _
  bind := _
}

partial def Std.CodeAction.instanceStub.collectFields (env : Lean.Environment) (structName : Lean.Name) (fields : Array Lean.Name) : Array Lean.Name

Returns the fields of a structure, unfolding parent structures.

def Std.CodeAction.getExplicitArgs : Lean.Expr → Array Lean.Name → Array Lean.Name

Returns the explicit arguments given a type.

Equations

• Std.CodeAction.getExplicitArgs (Lean.Expr.forallE n binderType body bi) x = Std.CodeAction.getExplicitArgs body (if Lean.BinderInfo.isExplicit bi = true then Array.push x n else x)
• Std.CodeAction.getExplicitArgs x x = x

def Std.CodeAction.eqnStub : Std.CodeAction.HoleCodeAction

Invoking hole code action "Generate a list of equations for a recursive definition" in the following:

def foo : Expr → Unit := _

produces:

def foo : Expr → Unit := fun
  | .bvar deBruijnIndex => _
  | .fvar fvarId => _
  | .mvar mvarId => _
  | .sort u => _
  | .const declName us => _
  | .app fn arg => _
  | .lam binderName binderType body binderInfo => _
  | .forallE binderName binderType body binderInfo => _
  | .letE declName type value body nonDep => _
  | .lit _ => _
  | .mdata data expr => _
  | .proj typeName idx struct => _

def Std.CodeAction.startTacticStub : Std.CodeAction.HoleCodeAction

Invoking hole code action "Start a tactic proof" will fill in a hole with by done.

def Std.CodeAction.removeAfterDoneAction : Std.CodeAction.TacticCodeAction

The "Remove tactics after 'no goals'" code action deletes any tactics following a completed proof.

example : True := by
  trivial
  trivial -- <- remove this, proof is already done
  rfl

is transformed to

example : True := by
  trivial

def Std.CodeAction.getElimNames (declName : Lean.Name) : Lean.MetaM (Array (Lean.Name × Array Lean.Name))

Similar to getElabInfo, but returns the names of binders instead of just the numbers; intended for code actions which need to name the binders.

def Std.CodeAction.casesExpand : Std.CodeAction.TacticCodeAction

Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the following:

example (x : Nat) : x = x := by
  induction x

produces:

example (x : Nat) : x = x := by
  induction x with
  | zero => sorry
  | succ n ih => sorry

It also works for cases.

def Std.CodeAction.addSubgoalsActionCore (params : Lean.Lsp.CodeActionParams) (i : Nat) (stk : Lean.Syntax.Stack) (goals : List Lean.MVarId) : Lean.Server.RequestM (Array Lean.Server.LazyCodeAction)

The "Add subgoals" code action puts · done subgoals for any goals remaining at the end of a proof.

example : True ∧ True := by
  constructor
  -- <- here

is transformed to

example : True ∧ True := by
  constructor
  · done
  · done

def Std.CodeAction.addSubgoalsSeqAction : Std.CodeAction.TacticSeqCodeAction

The "Add subgoals" code action puts · done subgoals for any goals remaining at the end of a proof.

example : True ∧ True := by
  constructor
  -- <- here

is transformed to

example : True ∧ True := by
  constructor
  · done
  · done

def Std.CodeAction.addSubgoalsAction : Std.CodeAction.TacticCodeAction

The "Add subgoals" code action puts · done subgoals for any goals remaining at the end of a proof.

example : True ∧ True := by
  constructor
  -- <- here

is transformed to

example : True ∧ True := by
  constructor
  · done
  · done