[−][src]Module tptp::syntax
Parsed syntactic structures
Structs
| Annotations | Formula annotations |
| CnfFormula | A CNF formula |
| Included | An include path, not including outer quotes |
Enums
| AssocConnective | An associative binary operator on FOF formulae |
| CnfLiteral | A CNF literal |
| DagSource | DAG formula sources |
| ExternalSource | External formula sources |
| FofFormula | A FOF formula |
| FofQuantifier | A FOF quantifier |
| FofTerm | A FOF term. |
| FormulaRole | A TPTP formula role, such as |
| InfixEquality | An infix binary operator on FOF terms |
| InternalSource | Internal formula sources |
| Name | One of various types of TPTP identifiers. |
| NonAssocConnective | A non-associative binary operator on FOF formulae |
| Source | Formula sources for use in annotations |
| Statement | A top-level TPTP statement, currently |
| UnaryConnective | A unary operator on FOF formulae |