On 2/11/23 07:39, David A. Wheeler wrote:
1) I think one of the "key" missing things is ability to help a user to understand why a statement doesn't unify.
I have only an approximate idea of whether this is easy or hard, but I will say that even modest improvements here would be helpful. For example, it may be easier to detect particular cases than every possible "way" a statement can't unify. One of the more time consuming things that happens to me when using mmj2 is that a unification which I expected to happen doesn't, and then I need to look at (sometimes long) expressions to figure out what parts don't match.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f4279719-c618-69f3-f70a-ce21902ebe8f%40panix.com.
