Index of modules

Comand-line interface for module Main.

Lexer for parsing formula strings.

For parsing, printing, and manipulating formulas.

Parser for mapping formula strings to objects of type FML_types.t_fml.

The abstract formula type (and its sub-types).

For handling input from files and stdin, and output to stdout and stderr.

Lexer for parsing deinitions and proofs (items).

For expanding formulas and proofs containing defined expressions, replacing each defined expression with its defining expression.

Parser for mapping files containing definitions and proofs to objects of type ITM_types.t_itm list.

The abstract type of definitions and proofs (items).

For validating natural deduction proofs in first-order { classical | intuitionistic | minimal } logic.

Lexer for parsing objects of type PRF_sequencer.t_prf_seq.

For parsing, printing, and manipulating proofs.

Parser for mapping objects of type PRF_sequencer.t_prf_seq to objects of type PRF_types.t_prf_raw.

For mapping two-dimensional natural deduction proof trees onto one-dimensional proof sequences of type PRF_sequencer.t_prf_seq.

The abstract proof types (and their sub-types).

For splitting strings into utf-8 grapheme clusters.