In my opinion, mmj2 is readable code. If I'm not mistaken, some code is spent on computing max array size. Since some code is old, it may be Java back then didn't have the variable length ADTs it has today.
w.r.t. the unification algorithm, I'm pretty sure there's a comment where Mel writes he's using Robinson's mgu finder. BR Glauco -- 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/9647953d-e719-4442-bf1a-ea65481ace66n%40googlegroups.com.
