MakeRE.Convval are_convertible : Kernel.Reduction.convertibility_testare_convertible sg t1 t2 checks whether t1 and t2 are convertible or not in the signature sg.
val constraint_convertibility :
Kernel.Rule.constr ->
Kernel.Rule.rule_name ->
Kernel.Reduction.convertibility_testconstraint_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 :
Kernel.Signature.t ->
(Kernel.Term.term * Kernel.Term.term) ->
(Kernel.Term.term * Kernel.Term.term) list ->
(Kernel.Term.term * Kernel.Term.term) listconversion_step sg (l,r) lst returns a list lst' containing new convertibility obligations. Raise NotConvertible if the two terms are not convertible.