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.

Equations

• One or more equations did not get rendered due to their size.

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 := _

Equations

• One or more equations did not get rendered due to their size.

def Batteries.CodeAction.instanceStub.isAutofillable (env : Lean.Environment) (fieldInfo : Lean.StructureFieldInfo) (stack : List Lean.Name) : Bool

Returns true if this field is an autoParam or optParam, or if it is given an optional value in a child struct.

Equations

• One or more equations did not get rendered due to their size.

partial def Batteries.CodeAction.instanceStub.collectFields (env : Lean.Environment) (structName : Lean.Name) (fields : Array (Lean.Name × Bool)) (stack : List Lean.Name) : Array (Lean.Name × Bool)

Returns the fields of a structure, unfolding parent structures.

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

Returns the explicit arguments given a type.

Equations

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

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 => _

Equations

• One or more equations did not get rendered due to their size.

def Batteries.CodeAction.startTacticStub : Lean.CodeAction.HoleCodeAction

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

Equations

• One or more equations did not get rendered due to their size.

def Batteries.CodeAction.removeAfterDoneAction : Batteries.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

Equations

• One or more equations did not get rendered due to their size.
• Batteries.CodeAction.removeAfterDoneAction x✝¹ x✝ x stk node = pure #[]

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.

Equations

• One or more equations did not get rendered due to their size.

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

Finds the TermInfo for an elaborated term stx.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Batteries.CodeAction.casesExpand x✝ snap ctx x node = pure #[]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Batteries.CodeAction.addSubgoalsSeqAction params x✝ x = Batteries.CodeAction.addSubgoalsActionCore params

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

Equations

• One or more equations did not get rendered due to their size.