Hi all, much thanks for all the useful feedback. On Saturday, June 7, 2025 at 2:03:04 PM UTC+2 Thierry Arnoux wrote:
In terms of features I'm missing, I would really like to have the "select smallest class/wff" feature I had in Emetamath. This should not be too hard, and I think this would be of great help. That's a great feature suggestion. It's on my do-to list! Are you using metamath-rs <https://github.com/metamath/metamath-knife/tree/main/metamath-rs> as a library or rewriting it from scratch? Is the project going to be open source? As of right now I am not using metamath-rs, since I thought that writing everything from scratch would make the project more independent (and more fun). I'm not sure whether mmt1 will be open-source yet, mainly because I've never led an open-source project so far. It's definitely going to be source-available and MIT-licensed though. Best regards, Marlo -- 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 visit https://groups.google.com/d/msgid/metamath/4873e158-8f4f-4e28-934d-63de9b2d7c4dn%40googlegroups.com.
