Parameter Make.C

val are_convertible : convertibility_test

are_convertible sg t1 t2 checks whether t1 and t2 are convertible or not in the signature sg.

val constraint_convertibility : Rule.constr -> Rule.rule_name -> convertibility_test

constraint_convertibility cstr r sg [t1] [t2] checks wehther the [cstr] of the rule [r] is satisfiable. Because constraints are checked once a term has matched the pattern, satisfying a constraint comes back to check that two terms are convertible

val conversion_step : Signature.t -> (Term.term * Term.term) -> (Term.term * Term.term) list -> (Term.term * Term.term) list

conversion_step sg (l,r) lst returns a list lst' containing new convertibility obligations. Raise NotConvertible if the two terms are not convertible.