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

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

Equations

• Batteries.CodeAction.isMatchTerm (Lean.Elab.Info.ofTermInfo i) = i.stx.isOfKind `Lean.Parser.Term.match
• Batteries.CodeAction.isMatchTerm x✝ = false

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

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

Equations

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

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.

Equations

• Batteries.CodeAction.findAllInfos p t = Batteries.CodeAction.findAllInfos.loop p t #[]

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.hasImplicitNonparArg (ctor : Lean.Name) (env : Lean.Environment) : Bool

Computes for a constructor, if it makes sense to use @constr in a match, by determining if it has any non-parameter implicit arguments.

Equations

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

def Batteries.CodeAction.patternFromConstructor (ctor : Lean.Name) (env : Lean.Environment) (suffix : String) (explicitArgsOnly ctor_hasImplicitNonparArg : Bool) : 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.

Equations

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

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

If it makes sense to use at least one of the constructors with @ (i.e. iff it has an implicit non-parameter argument) then we also show a codeaction that expands every such constructor with implicit arguments filled in with the syntax implicitArg := implicitArg. E.g. invoking Generate a list of equations with implicit arguments for this match. in the following

inductive TermWithImplicit (F : Nat → Type u) (α : Type w)
  | var (x : α) : TermWithImplicit F α
  | func {l : Nat} (f : F l) (ts : Fin l → TermWithImplicit F α) : TermWithImplicit F α

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with

produces

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with
  | .var x => _
  | .func (l := l) f ts => _

where the implicit argument {l : Nat} is now usable. Note that the arguments F and α are not filled since they are parameters (a parameter is an argument to an inductive type that is fixed over constructors), i.e. they are already determined by the match discriminant t. This means they don't provide any new information for you.

Equations

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