Index of values

Maps common notational variants of logical and mathematical terms to their canonical counterparts, e.g.

= {
        verbose = false;
        discharge = false;
        undischarge = false;
        logic = Classical;
        quiet = false;
}

expand_and_validate_file options path applies ITM_main.expand_file to path and checks validity of each expanded proof according to options.

expand_file path evaluates to expand_items (items_of_file path).

Recursively expands each item on a list according to the definitions preceding it (with the most immediate predecessors being applied first).

fml_is_fml_with_var_replaced_by_term fml1 fml2 var evaluates to Some term, if term is the first element of closed_terms_of_fml fml1 such that fml1 = subst_in_fml var term fml2 evaluates to true, and to None if no such element exists.

fml_list_of_file path applies fml_of_string to each line of the file located at path.

fml_of_fml_raw fml_raw evaluates to

match fml_raw with
|Fml_raw (s : string) -> FML_main.fml_of_string s

fml_of_string fml evaluates to an object of type FML_types.t_fml if fml conforms to the grammar specified in fml.txt, and raises exception Parse_error fml otherwise.

If path is the path of a file whose content conforms to the grammar specified in items.txt, then items_of_file path evaluates to a list of type ITM_types.t_itm, and otherwise raises an exception.

lexer_of_file path evaluates to lexer_of_matrix (matrix_of_file path).

lexer_of_matrix m evaluates to lexer_of_matrix ~print_trace:false ~automaton:default_automaton m.

lexer_of_string s evaluates to lexer_of_matrix (matrix_of_string s).

Same as matrix_of_string, but reads string from file located at the provided path.

matrix_of_string s forms rows by splitting s on character '\n', forms columns by applying UTF8_segmenter.utf_8_grapheme_clusters to each row, and converts the result to arrays.

premises_of_prf excluded prf evaluates to a non-repeating list of all undischarged assumptions of prf, except for those in excluded.

prf_of_file path evaluates to prf_of_prf_raw (prf_raw_of_file path).

prf_of_prf_raw prf_raw evaluates to the result of applying fml_of_fml_raw to each formula in prf_raw.

prf_of_stdin () evaluates to prf_of_prf_raw (prf_raw_of_stdin ()).

prf_of_string s evaluates to prf_of_prf_raw (prf_raw_of_string s).

Same as prf_raw_of_string, but reads from the file located at the given path.

prf_raw_of_prf_seq (Prf_seq s) evaluates (essentially) to PRF_parser.main PRF_lexer.token (Lexing.from_string s).

Same as prf_raw_of_string, but reads from stdin.

prf_raw_of_string s evaluates (essentially) to prf_raw_of_prf_seq (PRF_sequencer.prf_seq_of_string s).

Same as PRF_sequencer.prf_seq_of_string, but reads from the file located at the provided path.

prf_seq_of_string prf_tree evaluates to Prf_seq (String.concat "" (List.map string_of_token (lexer_of_string s))).

string_of_token token evaluates to

        match token with
        |FML_LETTER s -> s
        |RULE_LETTER s -> s
        |HSEP -> ";"
        |RSEP n -> "#" ^ (string_of_int n)
        |VSEP -> ":"

subst_free_vars_in_fml_with_terms subst fml evaluates to the result of simultaneously replacing every free variable in fml with a term according to the function subst: t_var -> t_term.

subst_in_fml var term fml evaluates to the result of replacing every free occurrence of var in fml with term, regardless of whether term contains variables that become bound.

subst_in_prf subst prf evaluates to the result of simultaneously replacing every atomic proof (undischarged assumption) in prf with another proof according to the function subst : t_prf -> t_prf.

transform_prf subst prf evaluates to the result of applying the function subst : t_fml -> t_fml to each formula in prf.

Maps "≠" to "=", for instance.

evaluates to utf_8_segments `Grapheme_cluster.

Splits a string by Uuseg.boundary.

validate_file options path evaluates to validate_prf options (PRF_main.prf_of_file path).

validate_prf prf evaluates to Some prf if prf represents a valid proof in classical first-order logic, and to None otherwise.

validate_stdin options () evaluates to validate_prf options (PRF_main.prf_of_stdin()).

Recursively lists all variables occurring in a list of terms.