Whoa! And I'm already spoiled by what Leo is doing with Lean 4. The so small core language and vastly extensible parser with an entire automation library for building and proving formal systems using incremental compilation with plans for interactive compiler guidance are mind blowing. That's taking aside your own exciting MM0 work. And I only have that much time to learn about lots of things. I'm torn already :(
-- 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/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com.
