Petrica Chiriac (Jan 09 2021 at 07:42):
Do we have a REPL (read–eval–print loop) for lean4? or is there a plan to exist?
Kenny Lau (Jan 09 2021 at 07:54):
The ability to use that would require typing a line of code perfectly without looking at the error message, which I believe only a handful in this community can do.
Joe Hendrix (Jan 09 2021 at 08:18):
There is not a REPL nor plans to write one afaik. I think it would have very limited utility.
I had thought I wanted a REPL when I first started using Lean, but once you have development environment integration working there isn't a need. If you want to interactively evaluate a term or print the type of an expression it is easier to quickly type commands like
#check in your buffer then to switch to a terminal and use a REPL.
Johan Commelin (Jan 09 2021 at 08:19):
#eval foo updates automatically when you tweak
foo. Continuous compilation is awesome.
Last updated: May 18 2021 at 23:14 UTC