package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
doc/logtk.parsers/Logtk_parsers/Parse_tptp/index.html
Module Logtk_parsers.Parse_tptp
type token = | XOR| WILDCARD| VLINE| UPPER_WORD of string| UNDERSCORE| TYPE_TY| TRUE| THF| TFF| STAR| SINGLE_QUOTED of string| RIGHT_PAREN| RIGHT_BRACKET| REAL of string| RATIONAL of string| NOT_EQUAL| NOTVLINE| NOTCONST| NOTAND| NOT| LOWER_WORD of string| LEFT_PAREN| LEFT_IMPLY| LEFT_BRACKET| LAMBDA| ITE| INTEGER of string| INCLUDE| IMPLYCONST| IMPLY| FORALL_TY| FORALLCONST| FORALL| FOF| FALSE| EXISTSCONST| EXISTS| EQUIV| EQUAL| EOI| DOT| DOLLAR_WORD of string| DOLLAR_DOLLAR_WORD of string| DISTINCT_OBJECT of string| COMMA| COLUMN| CNF| CHOICE_CONST| CHOICE_BINDER| AT| ARROW| AND
val parse_term : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Logtk.STerm.tval parse_formula : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Logtk.STerm.tval parse_declarations :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.STerm.t Ast_tptp.declaration listval parse_declaration :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.STerm.t Ast_tptp.declarationval parse_answer_tuple :
(Lexing.lexbuf -> token) ->
Lexing.lexbuf ->
Logtk.STerm.t list list