module Ast_tptp: sig
.. end
TPTP Ast
type
name =
| |
NameInt of int |
| |
NameString of string |
type
role =
| |
R_axiom |
| |
R_hypothesis |
| |
R_definition |
| |
R_assumption |
| |
R_lemma |
| |
R_theorem |
| |
R_conjecture |
| |
R_negated_conjecture |
| |
R_plain |
| |
R_finite of string |
| |
R_question |
| |
R_type |
| |
R_unknown |
type
optional_info = general_data list
formula role
type
general_data =
val role_of_string : string -> role
val string_of_role : role -> string
val pp_role : role CCFormat.printer
val string_of_name : name -> string
val pp_name : name CCFormat.printer
val pp_general : general_data CCFormat.printer
val pp_general_debugf : general_data CCFormat.printer
val pp_generals : general_data list CCFormat.printer
type 'a
t =
top level declaration
type 'a
declaration = 'a t
val get_name : 'a t -> name
Find the name of the declaration, or
Raises Invalid_argument
if the declaration is an include directive
IO
include Interfaces.PRINT1