## Stream: lean4

### Topic: REPL

#### 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 #eval or #check in your buffer then to switch to a terminal and use a REPL.

#### Johan Commelin (Jan 09 2021 at 08:19):

Also #eval foo updates automatically when you tweak foo. Continuous compilation is awesome.

Last updated: May 18 2021 at 23:14 UTC