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

Maintainers

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

Sources

1.5.1.tar.gz
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2

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