Hi Frédéric, I agree more explanations would help, I also needed time myself to get familiar with those definitions.
Would you mind proposing the additional text for the comments to those definitions? I can then help doing the actual changes in set.mm if needed. BR, _ Thierry -- 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/44dee908-e5df-976d-eb0e-7910e0bcc70c%40gmx.net.
