> Rust isn't a functional programming language, but the first implementation > of MM1 was in Haskell and it had some memory usage and speed issues that > would have required some significant concessions to imperative style to fix. >
Too bad for Haskell I'd guess. I don't think that there is no solution, here's how Lean 4 deals with similar problem: https://arxiv.org/abs/2003.01685 -- 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/daca05a9-b73b-4ff9-8dd6-a24e17beec02n%40googlegroups.com.
