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

Maintainers

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_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