package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63
doc/logtk/Logtk/UntypedAST/index.html
Module Logtk.UntypedAST
Main AST before Typing
Parsers eventually output this AST, that uses simple terms (STerm
) for types, terms, and formulas.
Everything is possibly annotated with a parse location so that error messages can be properly localized.
module Loc = ParseLocation
module T = STerm
type term = T.t
type ty = T.t
type form = T.t
type data = {
data_name : string;
data_vars : string list;
data_cstors : (string * (string option * ty) list) list;
}
Basic definition of inductive types
Attributes (general terms)
type attrs = attr list
val default_attrs : attrs
val name_of_attrs : attrs -> string option
val name : statement -> string option
module A : sig ... end
val attr_name : string -> attr
val attr_ac : attr
val attr_prefix : string -> attr
val attr_infix : string -> attr
val pp_attr : attr CCFormat.printer
val pp_attrs : attrs CCFormat.printer
val pp_attr_zf : attr CCFormat.printer
val pp_attrs_zf : attrs CCFormat.printer
val pp_attr_tstp : attr CCFormat.printer
Print as a TPTP general_term
val pp_statement : statement CCFormat.printer
Errors
exception Parse_error of Loc.t * string
val error : Loc.t -> string -> 'a
val errorf : Loc.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page