Module Srcheck.SRCheckerSource

Parameters

module R : Reduction.S

Signature

Sourcetype lhs_typing_cstr

Representation of LHS typing constraints

Sourceval pp_lhs_typing_cstr : lhs_typing_cstr Basic.printer

No constraints

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

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

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