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/Compute_prec/index.html
Module Logtk.Compute_prec
Compute Precedence
This module computes precedences that satisfy a list of constraints. See Precedence.Constr
for more details on constraints.
val empty : t
val add_constr : int -> [ `partial ] Precedence.Constr.t -> t -> t
Add a precedence constraint with its priority. The lower the priority, the stronger influence the constraint will have.
val add_constrs : (int * [ `partial ] Precedence.Constr.t) list -> t -> t
type 'a parametrized = Statement.clause_t Iter.t -> 'a
Some values are parametrized by the list of statements
val add_constr_rule :
int ->
[ `partial ] Precedence.Constr.t parametrized ->
t ->
t
Add a precedence constraint rule
val set_weight_rule : Precedence.weight_fun parametrized -> t -> t
Choose the way weights are computed
val add_status : (ID.t * Precedence.symbol_status) list -> t -> t
Specify explicitly the status of some symbols
val mk_precedence :
db_w:int ->
lmb_w:int ->
signature:Signature.t ->
t ->
Statement.clause_t Iter.t ->
Precedence.t
Parameters db_w and lmb_w correspond to the weight de-Bruijn and lambda abstraction given for computation of KBO.
Make a precedence
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page