package dedukti

  1. Overview
  2. Docs


module R : Reduction.S


type lhs_typing_cstr

Representation of LHS typing constraints

val pp_lhs_typing_cstr : lhs_typing_cstr Basic.printer
val empty : lhs_typing_cstr

No constraints

Retrieve extended substitution

val 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

val 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.

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