package logtk

  1. Overview
  2. Docs
On This Page
  1. TPTP Ast
    1. IO
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

TPTP Ast

type name =
  1. | NameInt of int
  2. | NameString of string
    (*

    name of a formula

    *)
and role =
  1. | R_axiom
  2. | R_hypothesis
  3. | R_definition
  4. | R_assumption
  5. | R_lemma
  6. | R_theorem
  7. | R_conjecture
  8. | R_negated_conjecture
  9. | R_plain
  10. | R_finite of string
  11. | R_question
  12. | R_type
  13. | R_unknown
    (*

    formula role

    *)
and optional_info = general_data list
and general_data =
  1. | GString of string
  2. | GVar of string
  3. | GInt of int
  4. | GColumn of general_data * general_data
  5. | GNode of string * general_data list
  6. | GList of general_data list
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_debugf : general_data CCFormat.printer
val pp_generals : general_data list CCFormat.printer
type 'a t =
  1. | CNF of name * role * 'a list * optional_info
  2. | FOF of name * role * 'a * optional_info
  3. | TFF of name * role * 'a * optional_info
  4. | THF of name * role * 'a * optional_info
  5. | TypeDecl of name * string * 'a * optional_info
  6. | NewType of name * string * 'a * optional_info
  7. | Include of string
  8. | IncludeOnly of string * name list
    (*

    top level declaration

    *)
type 'a declaration = 'a t
val get_name : _ t -> name

Find the name of the declaration, or

IO

include Logtk.Interfaces.PRINT1 with type 'a t := 'a t
val to_string : 'a CCFormat.printer -> 'a t -> string