The conversion check has a strategy to unfold the LHS before the RHS when checking that two maybe applied different operators are convertible. When cloning a theory with the "theory T <- U" stanza, the RHS of the conversion is an alias to the RHS. By swapping the two arguments, the convertibility check is immediate, while on the other case, both hands will be normalized.
A proper way to solve this problem would be to have a more advanced unfold heuristic (by using a generation ID per operators or having more meta-information on the operators bodies)
strub
commented
3 months ago
The conversion check has a strategy to unfold the LHS before the RHS when checking that two maybe applied different operators are convertible. When cloning a theory with the "theory T <- U" stanza, the RHS of the conversion is an alias to the RHS. By swapping the two arguments, the convertibility check is immediate, while on the other case, both hands will be normalized.
A proper way to solve this problem would be to have a more advanced unfold heuristic (by using a generation ID per operators or having more meta-information on the operators bodies)