Allow elaboration of Config
arguments to tactics.
Equations
Instances For
Allow elaboration of ApplyRulesConfig
arguments to tactics.
Equations
Instances For
def
Lean.Elab.Tactic.SolveByElim.parseArgs
(s : Option (TSyntax `Lean.Parser.Tactic.SolveByElim.args))
:
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 t
in the arguments.
The third component should contain t
for each -t
in the arguments.
Equations
Instances For
Elaborator for apply_rules.
See Lean.MVarId.applyRules
for a MetaM
level analogue of this tactic.