Index of modules


A
Ast_dimacs
AST requirements for the Dimacs format.
Ast_smtlib
AST requirement for the Smtlib format.
Ast_tptp
The type of identifiers
Ast_zf
The type of identifiers

D
Dimacs
Dimacs language input

I
Id
Standard implementation of identifiers
Id_intf
Interfaces for Identifiers.
Incremental [Parse_intf.S]

L
Language_intf
Interface for Dolmen languages modules
Lex_intf
Interface for Dolmen lexers.
Lexer [Language_intf.S]
The Lexer module for the language.
Location_intf
Interface for file locations.
Logic
Logic languages for formal proofs

M
Make [Logic]
Make [Tptp]
Functor to generate a parser for the TPTP format.
Make [Zf]
Functor to generate a parser for the Zipperposition format.
Make [Smtlib]
Functor to generate a parser for the Smtlib format.
Make [Dimacs]
Functor to generate a parser for the dimacs format.
MenhirInterpreter [Parse_intf.S]

P
ParseLocation
Standard implementation of file locations.
Parse_intf
Interface for Dolmen parsers.
Parser [Language_intf.S]
The Parser module for the language.

S
Smtlib
Smtlib language input
Statement
Standard imlplementation of statements.
Stmt_intf
Interfaces for statements.

T
Term
Standard implementation of terms
Term_intf
Interfaces for Terms.
Tptp
TPTP language input

Z
Zf
Zipperposition format input