Documentation

Lean.Elab.Tactic.SolveByElim

Allow elaboration of Config arguments to tactics.

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

    Allow elaboration of ApplyRulesConfig arguments to tactics.

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

      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
      • One or more equations did not get rendered due to their size.
      Instances For
        def Lean.Elab.Tactic.SolveByElim.parseUsing (s : Option (Lean.TSyntax `Lean.Parser.Tactic.SolveByElim.using_)) :

        Parse the using ... argument for solve_by_elim.

        Equations
        Instances For
          def Lean.Elab.Tactic.SolveByElim.processSyntax (cfg : optParam 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 : Bool) (star : Bool) (add : List Lean.Term) (remove : List Lean.Term) (use : Array Lean.Ident) (goals : List Lean.MVarId) :

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

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

              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.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For