package logtk
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63
doc/logtk.parsers/Logtk_parsers/Ast_dk/index.html
Module Logtk_parsers.Ast_dk
AST utils for dedukti
module A = Logtk.UntypedAST
module T = Logtk.STerm
include module type of struct include T end
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 = Logtk.ParseLocation.t
and match_branch = Logtk.STerm.match_branch =
and view = Logtk.STerm.view =
| Var of var
(*variable
*)| Const of string
(*constant
*)| AppBuiltin of Logtk.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
| Bind of Logtk.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 Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ with type t := t
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
val v_wild : t
wildcard
val builtin : ?loc:location -> Logtk.Builtin.t -> t
val app_builtin : ?loc:location -> Logtk.Builtin.t -> t list -> t
val bind : ?loc:location -> Logtk.Binder.t -> typed_var list -> t -> t
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 true_ : t
val false_ : t
val of_int : int -> 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
val unfold_bind : Logtk.Binder.t -> t -> typed_var list * t
module Set = T.Set
module Map = T.Map
module Tbl = T.Tbl
module StringSet = T.StringSet
module Seq = T.Seq
val ground : t -> bool
val close_all : Logtk.Binder.t -> t -> t
Bind all free vars with the symbol
include Logtk.Interfaces.PRINT with type t := t
val pp : t CCFormat.printer
val to_string : t -> string
val pp_typed_var : typed_var CCFormat.printer
val pp_var : var CCFormat.printer
Formats
module TPTP = T.TPTP
module TPTP_THF = T.TPTP_THF
module ZF = T.ZF
val pp_in : Logtk.Output_format.t -> t CCFormat.printer
Subst
module StrMap = T.StrMap
val empty_subst : subst
merge a b
merges a
into b
, but favors b
in case of conflict
type statement = Logtk.UntypedAST.statement
type ty = T.t
val const : string -> T.t
val mk_const_t : string -> term
val var : string -> T.t
val mk_var_t : string -> term
val v : string -> var
val add_alias : string -> T.t -> unit
val type_nat : term
exception Application_head_is_not_a_var of term
val mk_fun : T.typed_var list -> T.t -> T.t
val mk_forall : T.typed_var list -> T.t -> T.t
val mk_int : string -> T.t
val ty_prop : T.t
val mk_ty_decl : ?loc:A.Loc.t -> string -> A.ty -> A.statement
val mk_assert : ?loc:A.Loc.t -> name:string -> A.term -> A.statement
val mk_goal : ?loc:A.Loc.t -> name:string -> A.term -> A.statement
val mk_def : ?loc:A.Loc.t -> string -> A.ty -> T.t -> A.statement
val mk_rewrite : ?loc:A.Loc.t -> A.term -> A.statement
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page