Auto.Solver.TPTP

source

opaque auto.tptp :

Lean.Option Bool

source

opaque auto.tptp.trust :

Lean.Option Bool

source

axiom autoTPTPSorry (α : Sort u) :

α

source

opaque auto.tptp.premiseSelection :

Lean.Option Bool

source

opaque auto.tptp.timeout :

Lean.Option Nat

source

inductive Auto.Solver.TPTP.ZEPortType :

Type

fo : ZEPortType
lams : ZEPortType

Instances For

source

instance Auto.Solver.TPTP.instBEqZEPortType :

BEq ZEPortType

Equations

Auto.Solver.TPTP.instBEqZEPortType = { beq := Auto.Solver.TPTP.instBEqZEPortType.beq }

source

def Auto.Solver.TPTP.instBEqZEPortType.beq :

ZEPortType → ZEPortType → Bool

Equations

Auto.Solver.TPTP.instBEqZEPortType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Auto.Solver.TPTP.instHashableZEPortType :

Hashable ZEPortType

Equations

Auto.Solver.TPTP.instHashableZEPortType = { hash := Auto.Solver.TPTP.instHashableZEPortType.hash }

source

def Auto.Solver.TPTP.instHashableZEPortType.hash :

ZEPortType → UInt64

Equations

Instances For

source

def Auto.Solver.TPTP.instInhabitedZEPortType.default :

ZEPortType

Equations

Auto.Solver.TPTP.instInhabitedZEPortType.default = Auto.Solver.TPTP.ZEPortType.fo

Instances For

source

instance Auto.Solver.TPTP.instInhabitedZEPortType :

Inhabited ZEPortType

Equations

Auto.Solver.TPTP.instInhabitedZEPortType = { default := Auto.Solver.TPTP.instInhabitedZEPortType.default }

source

instance Auto.Solver.TPTP.instReprZEPortType :

Repr ZEPortType

Equations

Auto.Solver.TPTP.instReprZEPortType = { reprPrec := Auto.Solver.TPTP.instReprZEPortType.repr }

source

def Auto.Solver.TPTP.instReprZEPortType.repr :

ZEPortType → Nat → Std.Format

Equations

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

Instances For

source

inductive Auto.Solver.TPTP.SolverName :

Type

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

Instances For

source

instance Auto.Solver.TPTP.instBEqSolverName :

BEq SolverName

Equations

Auto.Solver.TPTP.instBEqSolverName = { beq := Auto.Solver.TPTP.instBEqSolverName.beq }

source

instance Auto.Solver.TPTP.instHashableSolverName :

Hashable SolverName

Equations

Auto.Solver.TPTP.instHashableSolverName = { hash := Auto.Solver.TPTP.instHashableSolverName.hash }

source

instance Auto.Solver.TPTP.instInhabitedSolverName :

Inhabited SolverName

Equations

Auto.Solver.TPTP.instInhabitedSolverName = { default := Auto.Solver.TPTP.instInhabitedSolverName.default }

source

def Auto.Solver.TPTP.instInhabitedSolverName.default :

SolverName

Equations

Auto.Solver.TPTP.instInhabitedSolverName.default = Auto.Solver.TPTP.SolverName.zipperposition

Instances For

source

instance Auto.Solver.TPTP.instReprSolverName :

Repr SolverName

Equations

Auto.Solver.TPTP.instReprSolverName = { reprPrec := Auto.Solver.TPTP.instReprSolverName.repr }

source

def Auto.Solver.TPTP.instReprSolverName.repr :

SolverName → Nat → Std.Format

Equations

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

Instances For

source

instance Auto.Solver.TPTP.instToStringSolverName :

ToString SolverName

Equations

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

source

instance Auto.Solver.TPTP.instValueSolverName :

Lean.KVMap.Value SolverName

Equations

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

source

opaque auto.tptp.solver.name :

Lean.Option Auto.Solver.TPTP.SolverName

source

opaque auto.tptp.zipperposition.path :

Lean.Option String

source

opaque auto.tptp.zeport.path :

Lean.Option String

source

opaque auto.tptp.eproverHo.path :

Lean.Option String

source

opaque auto.tptp.vampire.path :

Lean.Option String

source

@[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 }

Instances For

source

def Auto.Solver.TPTP.queryZipperposition (query : String) :

Lean.MetaM (Bool × String)

Equations

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

Instances For

source

def Auto.Solver.TPTP.getZipperpositionExePath :

Lean.MetaM System.FilePath

Equations

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

Instances For

source

def Auto.Solver.TPTP.queryZipperpositionExe (query : String) :

Lean.MetaM (Bool × String)

Equations

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

Instances For

source

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.

Instances For

source

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

Instances For

source

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.

Instances For

source

def Auto.Solver.TPTP.queryE (query : String) :

Lean.MetaM (Bool × String)

Equations

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

Instances For

source

def Auto.Solver.TPTP.queryVampire (query : String) :

Lean.MetaM (Bool × String)

Equations

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

Instances For

source

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.

Instances For