opaque auto.tptp : Lean.Option Bool

opaque auto.tptp.trust : Lean.Option Bool

axiom autoTPTPSorry (α : Sort u) : α

opaque auto.tptp.premiseSelection : Lean.Option Bool

opaque auto.tptp.timeout : Lean.Option Nat

inductive Auto.Solver.TPTP.ZEPortType : Type

• fo : ZEPortType
• lams : ZEPortType

instance Auto.Solver.TPTP.instBEqZEPortType : BEq ZEPortType

Equations

• Auto.Solver.TPTP.instBEqZEPortType = { beq := Auto.Solver.TPTP.beqZEPortType✝ }

instance Auto.Solver.TPTP.instHashableZEPortType : Hashable ZEPortType

Equations

• Auto.Solver.TPTP.instHashableZEPortType = { hash := Auto.Solver.TPTP.hashZEPortType✝ }

instance Auto.Solver.TPTP.instInhabitedZEPortType : Inhabited ZEPortType

Equations

• Auto.Solver.TPTP.instInhabitedZEPortType = { default := Auto.Solver.TPTP.ZEPortType.fo }

instance Auto.Solver.TPTP.instReprZEPortType : Repr ZEPortType

Equations

• Auto.Solver.TPTP.instReprZEPortType = { reprPrec := Auto.Solver.TPTP.reprZEPortType✝ }

inductive Auto.Solver.TPTP.SolverName : Type

• zipperposition : SolverName
• zipperposition_exe : SolverName
• zeport (zept : ZEPortType) : SolverName
• eproverHo : SolverName
• vampire : SolverName

instance Auto.Solver.TPTP.instBEqSolverName : BEq SolverName

Equations

• Auto.Solver.TPTP.instBEqSolverName = { beq := Auto.Solver.TPTP.beqSolverName✝ }

instance Auto.Solver.TPTP.instHashableSolverName : Hashable SolverName

Equations

• Auto.Solver.TPTP.instHashableSolverName = { hash := Auto.Solver.TPTP.hashSolverName✝ }

instance Auto.Solver.TPTP.instInhabitedSolverName : Inhabited SolverName

Equations

• Auto.Solver.TPTP.instInhabitedSolverName = { default := Auto.Solver.TPTP.SolverName.zipperposition }

instance Auto.Solver.TPTP.instReprSolverName : Repr SolverName

Equations

• Auto.Solver.TPTP.instReprSolverName = { reprPrec := Auto.Solver.TPTP.reprSolverName✝ }

instance Auto.Solver.TPTP.instToStringSolverName : ToString SolverName

Equations

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

instance Auto.Solver.TPTP.instValueSolverName : Lean.KVMap.Value SolverName

Equations

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

opaque auto.tptp.solver.name : Lean.Option Auto.Solver.TPTP.SolverName

opaque auto.tptp.zipperposition.path : Lean.Option String

opaque auto.tptp.zeport.path : Lean.Option String

opaque auto.tptp.eproverHo.path : Lean.Option String

opaque auto.tptp.vampire.path : Lean.Option String

@[reducible, inline]

abbrev Auto.Solver.TPTP.SolverProc : Type

Equations

• Auto.Solver.TPTP.SolverProc = IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }

def Auto.Solver.TPTP.queryZipperposition (query : String) : Lean.MetaM (Bool × String)

Equations

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

def Auto.Solver.TPTP.getZipperpositionExePath : Lean.MetaM System.FilePath

Equations

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

def Auto.Solver.TPTP.queryZipperpositionExe (query : String) : Lean.MetaM (Bool × String)

Equations

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

def Auto.Solver.TPTP.queryZEPort (zept : ZEPortType) (query : String) : Lean.MetaM (Bool × String)

Equations

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

def Auto.Solver.TPTP.queryZEPort.attempt (action : Lean.MetaM Unit) : Lean.MetaM Unit

Equations

• Auto.Solver.TPTP.queryZEPort.attempt action = tryCatch action fun (x : Lean.Exception) => pure ()

def Auto.Solver.TPTP.queryZEPort.createSolver (zept : ZEPortType) (path : String) (idx : Nat) : Lean.MetaM SolverProc

Equations

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

def Auto.Solver.TPTP.queryE (query : String) : Lean.MetaM (Bool × String)

Equations

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

def Auto.Solver.TPTP.queryVampire (query : String) : Lean.MetaM (Bool × String)

Equations

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

def Auto.Solver.TPTP.querySolver (query : String) : Lean.MetaM (Bool × Array Parser.TPTP.Command)

Equations

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