Documentation

Lean.Elab.Tactic.SolveByElim

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 tin the arguments. The third component should contain t for each -t in the arguments.

          Equations
            Instances For
              def Lean.Elab.Tactic.SolveByElim.parseUsing (s : Option (TSyntax `Lean.Parser.Tactic.SolveByElim.using_)) :

              Parse the using ... argument for solve_by_elim.

              Equations
                Instances For

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

                  Equations
                    Instances For

                      Elaborator for apply_rules.

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

                      Equations
                        Instances For