On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Parameters
module R : Reduction.SSignature
val pp_lhs_typing_cstr : lhs_typing_cstr Basic.printerval empty : lhs_typing_cstrNo constraints
val get_subst : lhs_typing_cstr -> Exsubst.ExSubst.tRetrieve extended substitution
val get_unsat : lhs_typing_cstr -> Term.cstr optionIf no instance of the LHS is typable, output a witness that the rule cannot be triggered
val convertible :
Signature.t ->
lhs_typing_cstr ->
int ->
Term.term ->
Term.term ->
boolconvertible sg c depth t u is true if the constraints c ensures that t and u, considered both under depth abstractions, are convertible
val compile_cstr : Signature.t -> Term.cstr list -> lhs_typing_cstrTransforms a list of constraints (ie equality between terms under abstractions), to a lhs_typing_cstr.
val optimize : Signature.t -> lhs_typing_cstr -> lhs_typing_cstrEquality inferred while assuming that the LHS is well-typed are put in normal form.
On This Page