package logtk

  1. Overview
  2. Docs
On This Page
  1. TPTP Ast
    1. IO
Core types and algorithms for logic

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

1.6.tar.gz
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d

doc/logtk.parsers/Logtk_parsers/Ast_tptp/index.html

Module Logtk_parsers.Ast_tptpSource

TPTP Ast

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

    name of a formula

    *)
Sourceand 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

    *)
Sourceand optional_info = general_data list
Sourceand 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
Sourceval role_of_string : string -> role
Sourceval string_of_role : role -> string
Sourceval string_of_name : name -> string
Sourceval pp_general_debugf : general_data CCFormat.printer
Sourceval pp_generals : general_data list CCFormat.printer
Sourcetype '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

    *)
Sourcetype 'a declaration = 'a t
Sourceval get_name : _ t -> name

Find the name of the declaration, or

IO

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