Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type tptp_input =
| Fof_anno of fof_formula annotated_formula
| Cnf_anno of cnf_formula annotated_formula
| Include of file_name * formula_name list
| Comment of comment_line
and !'t annotated_formula = {
af_name : formula_name;
af_role : formula_role;
af_formula : 't;
af_annos : annotations option;
}
and atomic_word =
| Plain_word of plain_word
| Defined_word of defined_word
| System_word of system_word
and file_name = plain_word
and gdata =
| G_func of plain_word * gterm list
| G_var of var
| G_number of Q.t
| G_string of tptp_string
| G_formula of gformula
val to_var : string -> var
val to_plain_word : string -> plain_word
val to_defined_word : string -> defined_word
val to_system_word : string -> system_word
val to_tptp_string : string -> tptp_string
val to_comment_line : string -> comment_line