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/Util_tptp/index.html
Module Logtk_parsers.Util_tptp
Utils related to TPTP
module A = Ast_tptp
type 'a or_error = ('a, string) CCResult.t
type untyped = Logtk.STerm.t
type typed = Logtk.TypedSTerm.t
val enable_def_as_rewrite : bool ref
Printing/Parsing
val create_parse_cache : unit -> parse_cache
find_file name dir
looks for a file with the given name
, recursively, in dir
, or in its parent dir recursively. It also looks in the "TPTP" environment variable.
val parse_lexbuf :
?names:A.name list ->
Lexing.lexbuf ->
untyped A.t Iter.t or_error
Given a lexbuf, try to parse its content into a sequence of untyped declarations
val parse_file :
?cache:parse_cache ->
recursive:bool ->
string ->
untyped A.t Iter.t or_error
Parsing a TPTP file is here presented with a recursive
option that, if true, will make "include" directives to be recursively parsed. It uses find_file
for included files.
Printing is simpler, because it does not involve includes.
val print_into : 't CCFormat.printer -> 't A.t Iter.t CCFormat.printer
val print_into_file : 't CCFormat.printer -> string -> 't A.t Iter.t -> unit
val has_includes : _ A.t Iter.t -> bool
Check whether some include declaration can be found in the sequence
Bridge to UntypedAST
val to_ast : untyped A.t -> Logtk.UntypedAST.statement
val of_ast : Logtk.UntypedAST.statement -> untyped A.t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page