TorchLean API

Docs HomeGuideExamplesGraphs

Lean.Elab.CheckTactic

Commands to validate tactic results.

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