def Batteries.CodeAction.isMatchTerm : Lean.Elab.Info → Bool

Filter for the info-nodes to find the match-nodes.

def Batteries.CodeAction.getMatchHeaderRange? (matchStx : Lean.Syntax) : Option String.Range

Returns the String.range that encompasses match e (with).

def Batteries.CodeAction.findAllInfos (p : Lean.Elab.Info → Bool) (t : Lean.Elab.InfoTree) : Array Lean.Elab.Info

Flattens an Infotree into an array of Info-nodes that fulfill p.

partial def Batteries.CodeAction.findAllInfos.loop (p : Lean.Elab.Info → Bool) (t : Lean.Elab.InfoTree) (acc : Array Lean.Elab.Info) : Array Lean.Elab.Info

Inner loop for findAllInfos.

def Batteries.CodeAction.pattern_from_constructor (ctor : Lean.Name) (env : Lean.Environment) (suffix : String) : Option String

From a constructor-name e.g. 'Option.some' construct the corresponding match pattern, e.g. '.some val'. We implement special cases for Nat and List, Option and Bool to e.g. produce 'n + 1' instead of 'Nat.succ n'.

def Batteries.CodeAction.matchExpand : Lean.CodeAction.CommandCodeAction

Invoking tactic code action "Generate a list of alternatives for this match." in the following:

def myfun2 (n : Nat) : Nat :=
  match n

produces:

def myfun2 (n : Nat) : Nat :=
  match n with
  | 0 => _
  | n + 1 => _

Also has support for multiple discriminants, e.g.

def myfun3 (o : Option Bool) (m : Nat) : Nat :=
  match o, m with

can be expanded into

def myfun3 (o : Option Bool) (m : Nat) : Nat :=
  match o, m with
  | none, 0 => _
  | none, n_2 + 1 => _
  | some val_1, 0 => _
  | some val_1, n_2 + 1 => _