def Lean.Elab.Tactic.SolveByElim.elabConfig (cfg : Syntax) (init : Meta.SolveByElim.SolveByElimConfig := { }) (logExceptions : Bool := true) : TacticM Meta.SolveByElim.SolveByElimConfig

Allow elaboration of Config arguments to tactics.

Note: does not generate a (config := ...) option due to the fields in the omit clause, which are all function-valued and have no EvalExpr instances.

def Lean.Elab.Tactic.SolveByElim.elabApplyRulesConfig (cfg : Syntax) (init : Meta.SolveByElim.ApplyRulesConfig := { }) (logExceptions : Bool := true) : TacticM Meta.SolveByElim.ApplyRulesConfig

Allow elaboration of ApplyRulesConfig arguments to tactics.

Note: does not generate a (config := ...) option due to the fields in the omit clause, which are all function-valued and have no EvalExpr instances.

def Lean.Elab.Tactic.SolveByElim.parseArgs (s : Option (TSyntax `Lean.Parser.Tactic.SolveByElim.args)) : Bool × List Term × List Term

Parse the lemma argument of a call to solve_by_elim. The first component should be true if * appears at least once. The second component should contain each term tin the arguments. The third component should contain t for each -t in the arguments.

def Lean.Elab.Tactic.SolveByElim.parseUsing (s : Option (TSyntax `Lean.Parser.Tactic.SolveByElim.using_)) : Array Ident

Parse the using ... argument for solve_by_elim.

def Lean.Elab.Tactic.SolveByElim.processSyntax (cfg : Meta.SolveByElim.SolveByElimConfig := { }) (only star : Bool) (add remove : List Term) (use : Array Ident) (goals : List MVarId) : MetaM (List MVarId)

Wrapper for solveByElim that processes a list of Terms that specify the lemmas to use.

def Lean.Elab.Tactic.SolveByElim.evalApplyAssumption : Tactic

def Lean.Elab.Tactic.SolveByElim.evalApplyRules : Tactic

Elaborator for apply_rules.

See Lean.MVarId.applyRules for a MetaM level analogue of this tactic.

def Lean.Elab.Tactic.SolveByElim.evalSolveByElim : Tactic