Documentation

Lean.Elab.CheckTactic

Commands to validate tactic results.

source
def Lean.Elab.CheckTactic.elabCheckTactic :
Command.CommandElab
Equations
    Instances For
      source
      def Lean.Elab.CheckTactic.elabCheckTacticFailure :
      Command.CommandElab
      Equations
        Instances For
          source
          def Lean.Elab.CheckTactic.expandCheckSimp :
          Macro
          Equations
            Instances For
              source
              def Lean.Elab.CheckTactic.expandCheckSimpFailure :
              Macro
              Equations
                Instances For