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.instBEqSolverConfig.beq }

def EvalAuto.instBEqSolverConfig.beq : SolverConfig → SolverConfig → Bool

Equations

• EvalAuto.instBEqSolverConfig.beq EvalAuto.SolverConfig.native EvalAuto.SolverConfig.native = true
• EvalAuto.instBEqSolverConfig.beq EvalAuto.SolverConfig.rawNative EvalAuto.SolverConfig.rawNative = true
• EvalAuto.instBEqSolverConfig.beq EvalAuto.SolverConfig.leanSmt EvalAuto.SolverConfig.leanSmt = true
• EvalAuto.instBEqSolverConfig.beq (EvalAuto.SolverConfig.smt a) (EvalAuto.SolverConfig.smt b) = (a == b)
• EvalAuto.instBEqSolverConfig.beq (EvalAuto.SolverConfig.tptp a a_1) (EvalAuto.SolverConfig.tptp b b_1) = (a == b && a_1 == b_1)
• EvalAuto.instBEqSolverConfig.beq x✝¹ x✝ = false

def EvalAuto.instHashableSolverConfig.hash : SolverConfig → UInt64

Equations

• EvalAuto.instHashableSolverConfig.hash EvalAuto.SolverConfig.native = 0
• EvalAuto.instHashableSolverConfig.hash EvalAuto.SolverConfig.rawNative = 1
• EvalAuto.instHashableSolverConfig.hash EvalAuto.SolverConfig.leanSmt = 2
• EvalAuto.instHashableSolverConfig.hash (EvalAuto.SolverConfig.smt a) = mixHash 3 (hash a)
• EvalAuto.instHashableSolverConfig.hash (EvalAuto.SolverConfig.tptp a a_1) = mixHash (mixHash 4 (hash a)) (hash a_1)

instance EvalAuto.instHashableSolverConfig : Hashable SolverConfig

Equations

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

def EvalAuto.instReprSolverConfig.repr : SolverConfig → Nat → Std.Format

Equations

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

instance EvalAuto.instReprSolverConfig : Repr SolverConfig

Equations

• EvalAuto.instReprSolverConfig = { reprPrec := EvalAuto.instReprSolverConfig.repr }

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")