def Lean.Elab.Tactic.SolveByElim.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Meta.SolveByElim.SolveByElimConfig

Allow elaboration of Config arguments to tactics.

Equations

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

def Lean.Elab.Tactic.SolveByElim.elabApplyRulesConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Meta.SolveByElim.ApplyRulesConfig

Allow elaboration of ApplyRulesConfig arguments to tactics.

def Lean.Elab.Tactic.SolveByElim.parseArgs (s : Option (Lean.TSyntax `Lean.Parser.Tactic.SolveByElim.args)) : Bool × List Lean.Term × List Lean.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 (Lean.TSyntax `Lean.Parser.Tactic.SolveByElim.using_)) : Array Lean.Ident

Parse the using ... argument for solve_by_elim.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.SolveByElim.parseUsing none = #[]

def Lean.Elab.Tactic.SolveByElim.processSyntax (cfg : Lean.Meta.SolveByElim.SolveByElimConfig := { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (only star : Bool) (add remove : List Lean.Term) (use : Array Lean.Ident) (goals : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

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

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

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

Elaborator for apply_rules.

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

Equations

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

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

Equations

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