Hi Mario, Like many I'm following your developments with great interest, but I have not started playing with it.
I've been enjoying a lot developing proofs in MM using MMJ2. What would be the future of that? Do you expect that the tools in MM1 will be so advanced that people will prefer using MM1 instead of MM, or do you expect developments on set.mm (and iset.mm) to continue in the MM format? Will it be possible to have developments made in MM1 flow back into set.mm? In short, what would be the different development pipelines? * [MMJ2] MM -> MM0 -> publication in HOL/lean? * [mm0-hs] MM1 -> MM0 -> MM? Thanks, 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/c4c19f8c-5641-9489-12ae-5290bcdcdd17%40gmx.net.
