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.2.17@m4x.org

Sources

2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

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

Module Logtk_parsers.Ast_tptp

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