package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
doc/logtk/Logtk/STerm/index.html
Module Logtk.STerm
Simple Terms
Simple terms, that are not hashconsed, nor typed.
Those do not use De Bruijn indices for variable binding, but simply names (scoping is done later). Their simplicity make them good for heavy AST transformations, output of parsing, etc.
Terms are only compared, hashsed, etc. by their "term" component (the algebraic variant). Additional fields (location…) are ignored for almost every operation.
type location = ParseLocation.t
and view =
| Var of var
(*variable
*)| Const of string
(*constant
*)| AppBuiltin of Builtin.t * t list
| App of t * t list
(*apply term
*)| Ite of t * t * t
| Match of t * match_branch list
| Let of (var * t) list * t
| With of (var * t) list * t
| Bind of Binder.t * typed_var list * t
(*bind n variables
*)| List of t list
(*special constructor for lists
*)| Record of (string * t) list * var option
(*extensible record
*)
type term = t
include Interfaces.ORD with type t := t
val v_wild : t
wildcard
val match_ : ?loc:location -> t -> match_branch list -> t
val nil : t
val wildcard : t
val is_app : t -> bool
val is_var : t -> bool
val is_lam : t -> bool
val true_ : t
val false_ : t
val int_ : Logtk_arith.Z.t -> t
val of_int : int -> t
val rat : Logtk_arith.Q.t -> t
val real : string -> t
val tType : t
val term : t
val prop : t
val ty_int : t
val ty_rat : t
val ty_real : t
module Tbl : CCHashtbl.S with type key = term
module Seq : sig ... end
val ground : t -> bool
val pp_typed_var : typed_var CCFormat.printer
val pp_var : var CCFormat.printer
Formats
module TPTP : sig ... end
module TPTP_THF : sig ... end
module ZF : sig ... end
val pp_in : Output_format.t -> t CCFormat.printer
Subst
val empty_subst : subst
merge a b
merges a
into b
, but favors b
in case of conflict
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page