package universo

  1. Overview
  2. Docs

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

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

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

OCaml

Innovation. Community. Security.