grind parameter elaboration

def Lean.Meta.Grind.ExtensionStateArray.find (s : ExtensionStateArray) (origin : Origin) : List EMatchTheorem

Equations

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

def Lean.Elab.Tactic.addEMatchTheorem (params : Meta.Grind.Params) (id : Ident) (declName : Name) (kind : Meta.Grind.EMatchTheoremKind) (minIndexable : Bool) (suggest : Bool := false) (warn : Bool := true) : MetaM Meta.Grind.Params

Equations

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

def Lean.Elab.Tactic.elabGrindParams (params : Meta.Grind.Params) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (only : Bool) (lax incremental : Bool := false) : TermElabM Meta.Grind.Params

Elaborates grind parameters. incremental = true for tactics such as finish, in this case, we disable some kinds of parameters such as - ident.

Equations

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

def Lean.Elab.Tactic.Grind.getPreservedParams (params : Array (TSyntax `Lean.Parser.Tactic.grindParam)) : TermElabM (Array (TSyntax `Lean.Parser.Tactic.grindParam))

Returns the parameters of a grind?/finish? call that the suggested tactic must carry verbatim.

Parameters that produce E-matching theorems are recorded in the generated script as use/instantiate steps and are omitted. The remaining parameters have effects the script cannot represent, so dropping them produces suggestions that fail during replay:

• modifiers that do not create E-matching theorems (cases, inj, funCC, symbol);
• identifiers resolving to a type marked for case-splitting (e.g., [EqvGen] for an inductive predicate);
• identifiers resolving to a theorem whose statement is not a ∀ and is not indexable (see isFactDecl), which is asserted as a fact rather than recorded as an E-matching theorem;
• identifiers using local variable dot notation (e.g., cs.getD_rightInvSeq where cs is a local variable), which produce anchors that need the original term during replay;
• non-identifier terms (e.g., show p by tac).

TODO: This syntactic filtering is a stopgap: it duplicates parameter-elaboration logic and silently depends on which side effects are representable in scripts. A more robust solution is to make the script self-contained, e.g., a script step that marks a type for case-splitting, and tracking which parameters were actually used.

Equations

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

def Lean.Elab.Tactic.Grind.withParams {α : Type} (params : Meta.Grind.Params) (ps : TSyntaxArray `Lean.Parser.Tactic.grindParam) (only : Bool) (k : GrindTacticM α) : GrindTacticM α

Helper method for processing parameters in tactics such as finish and finish?

Equations

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