Topic: compiler backends
François Sunatori (Mar 06 2021 at 02:22):
Bryan Gin-ge Chen (Mar 06 2021 at 02:48):
There's nothing like that for Lean 3 (although you can run a WebAssembly version of the Lean 3 interpreter in the browser - see e.g. #webeditor).
Lean 4 can be compiled to C, though I don't think the details have been added to the docs yet.
François Sunatori (Mar 06 2021 at 04:29):
Bryan Gin-ge Chen (Mar 06 2021 at 04:32):
I don't know if anyone has done so yet, but I think a lot of folks are aiming to do that eventually. See e.g. this post.
(I'm probably not the right person to ask about this.)
Last updated: May 15 2021 at 00:39 UTC