package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

An implementation of The Lambda-Pi Modulo Theory

Install

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

module R : Reduction.S

Sourcetype lhs_typing_cstr

Representation of LHS typing constraints

Sourceval pp_lhs_typing_cstr : lhs_typing_cstr Basic.printer

Sourceval empty : lhs_typing_cstr

No constraints

Sourceval get_subst : lhs_typing_cstr -> Exsubst.ExSubst.t

Retrieve extended substitution

Sourceval get_unsat : lhs_typing_cstr -> Term.cstr option

If 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 ->
  bool

convertible sg c depth t u is true if the constraints c ensures that t and u, considered both under depth abstractions, are convertible

Sourceval compile_cstr : Signature.t -> Term.cstr list -> lhs_typing_cstr

Transforms a list of constraints (ie equality between terms under abstractions), to a lhs_typing_cstr.

Sourceval optimize : Signature.t -> lhs_typing_cstr -> lhs_typing_cstr

Equality inferred while assuming that the LHS is well-typed are put in normal form.

On This Page