lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard

Printing of unification rules fails

Open fblanqui opened this issue 2 years ago • 0 comments

Printing unification rules by using print unif_rule or verbose fails. The problem is in Term.term_of_rhs: r.arities.(i) is invalid if i corresponds to a RHS extra variable. Contrary to what is said in term.ml, r.arities does not provide the arities of the pattern variables bound in the RHS but those in the LHS only. And the arity is not recorded in scope.ml in the cases M_URHS. In the case of P_Wild, one could use List.length env.

fblanqui avatar Aug 01 '23 13:08 fblanqui