grind parameter elaboration

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) : MetaM 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.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.