Miscellaneous code actions

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

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

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

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

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

def Batteries.CodeAction.instanceStub : Lean.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 (minimal) skeleton for the structure under construction." produces:

instance : Monad Id where
  pure := _
  bind := _

and invoking "Generate a (maximal) skeleton for the structure under construction." produces:

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

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

Returns the explicit arguments given a type. The second argument of this function is an accumulator.

def Batteries.CodeAction.getAllArgs : Lean.Expr → Array Lean.Name → Array Lean.Name

Returns all of the arguments given a type. The second argument of this function is an accumulator.

def Batteries.CodeAction.eqnStub : Lean.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 Batteries.CodeAction.startTacticStub : Lean.CodeAction.HoleCodeAction

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

def Batteries.CodeAction.removeAfterDoneAction : 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 Batteries.CodeAction.getElimExprNames (elimType : Lean.Expr) : Lean.MetaM (Array (Lean.Name × Array Lean.Name))

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

def Batteries.CodeAction.findTermInfo? (node : Lean.Elab.InfoTree) (stx : Lean.Term) : Option Lean.Elab.TermInfo

Finds the TermInfo for an elaborated term stx.

def Batteries.CodeAction.casesExpand : 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 Batteries.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 Batteries.CodeAction.addSubgoalsSeqAction : 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 Batteries.CodeAction.addSubgoalsAction : 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