Documentation

Lean.Elab.Tactic.Decide

source
def Lean.Elab.Tactic.elabNativeDecideCore (tacticName : Name) (expectedType : Expr) :
TacticM Expr
Instances For
    source
    def Lean.Elab.Tactic.evalDecideCore (tacticName : Name) (cfg : Parser.Tactic.DecideConfig) :
    TacticM Unit
    Instances For
      source
      def Lean.Elab.Tactic.elabDecideConfig (cfg : Syntax) (init : Parser.Tactic.DecideConfig := { }) (logExceptions : Bool := true) :
      TacticM Parser.Tactic.DecideConfig
      Instances For
        source
        def Lean.Elab.Tactic.evalDecide :
        Tactic
        Instances For
          source
          def Lean.Elab.Tactic.evalNativeDecide :
          Tactic
          Instances For