package logtk

You can search for identifiers within the package.

in-package search v0.2.0

Core types and algorithms for logic

Install

Dune Dependency

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

Authors

S

Simon Cruanes

Maintainers

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_tptp`Source

TPTP Ast

Sourcetype name =

| NameInt of int
| NameString of string
(*
name of a formula
*)

Sourceand 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
(*
formula role
*)

Sourceand optional_info = general_data list

Sourceand general_data =

| GString of string
| GVar of string
| GInt of int
| GColumn of general_data * general_data
| GNode of string * general_data list
| GList of general_data list

Sourceval role_of_string : string -> role

Sourceval string_of_role : role -> string

Sourceval pp_role : role CCFormat.printer

Sourceval string_of_name : name -> string

Sourceval pp_name : name CCFormat.printer

Sourceval pp_general : general_data CCFormat.printer

Sourceval pp_general_debugf : general_data CCFormat.printer

Sourceval pp_generals : general_data list CCFormat.printer

Sourcetype 'a t =

| CNF of name * role * 'a list * optional_info
| FOF of name * role * 'a * optional_info
| TFF of name * role * 'a * optional_info
| THF of name * role * 'a * optional_info
| TypeDecl of name * string * 'a * optional_info
| NewType of name * string * 'a * optional_info
| Include of string
| 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

raises Invalid_argument
if the declaration is an include directive

IO

include Logtk.Interfaces.PRINT1 with type 'a t := 'a t

Sourceval pp : 'a CCFormat.printer -> 'a t CCFormat.printer

Sourceval to_string : 'a CCFormat.printer -> 'a t -> string

On This Page

TPTP Ast
1. IO