knuckledragger
kdrag
kdrag.all
kdrag.config
kdrag.kernel
kdrag.notation
kdrag.smt
kdrag.solvers
kdrag.solvers.binpath
kdrag.solvers.collect_decls
kdrag.solvers.collect_sorts
kdrag.solvers.expr_to_smtlib
kdrag.solvers.expr_to_tptp
expr_to_tptp()
kdrag.solvers.funcdecl_smtlib
kdrag.solvers.install_solvers
kdrag.solvers.mangle_decl
kdrag.solvers.run
kdrag.solvers.smtlib_datatypes
kdrag.solvers.sort_to_tptp
kdrag.solvers.egglog
kdrag.solvers.gappa
kdrag.tactics
kdrag.theories
kdrag.utils
knuckledragger
kdrag
kdrag.solvers
kdrag.solvers.expr_to_tptp
View page source
kdrag.solvers.expr_to_tptp
kdrag.solvers.
expr_to_tptp
(
expr
:
ExprRef
,
env
=
None
,
format
=
'thf'
,
theories
=
True
)
Pretty print expr as TPTP