inductive EvalAuto.SolverConfig : Type

• native : SolverConfig
• rawNative : SolverConfig
• leanSmt : SolverConfig
• smt (solverName : Auto.Solver.SMT.SolverName) : SolverConfig
• tptp (solverName : Auto.Solver.TPTP.SolverName) (path : String) : SolverConfig

instance EvalAuto.instBEqSolverConfig : BEq SolverConfig

Equations

• EvalAuto.instBEqSolverConfig = { beq := EvalAuto.beqSolverConfig✝ }

instance EvalAuto.instHashableSolverConfig : Hashable SolverConfig

Equations

• EvalAuto.instHashableSolverConfig = { hash := EvalAuto.hashSolverConfig✝ }

instance EvalAuto.instReprSolverConfig : Repr SolverConfig

Equations

• EvalAuto.instReprSolverConfig = { reprPrec := EvalAuto.reprSolverConfig✝ }

instance EvalAuto.instToStringSolverConfig : ToString SolverConfig

Equations

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

def EvalAuto.disableAllSolvers (o : Lean.Options) : Lean.Options

Equations

• EvalAuto.disableAllSolvers o = Lean.Option.set (Lean.Option.set (Lean.Option.set o auto.native false) auto.smt false) auto.tptp false

def EvalAuto.withAutoSolverConfigOptions {α : Type} {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadWithOptions m] [MonadControlT Lean.CoreM m] [MonadWithReaderOf Lean.Core.Context m] (config : SolverConfig) (timeout : Nat) (k : m α) : m α

Equations

• One or more equations did not get rendered due to their size.
• EvalAuto.withAutoSolverConfigOptions EvalAuto.SolverConfig.rawNative timeout k = k
• EvalAuto.withAutoSolverConfigOptions EvalAuto.SolverConfig.leanSmt timeout k = Lean.throwError (Lean.toMessageData "Lean-SMT is currently not supported")