lean REPL

Stream: general

[banach123]

Hello I wish to run a REPL but I can't seem to find any relevant options in lean --help could someone please help me out? I'm running a lean4

[Henrik Böving]

The answer to this is: You most likely do not wish to run a REPL but instead want to use Lean in interactive mode (if you are getting into Lean 4 and have more questions there is a dedicated Lean 4 stream by the way) via the vscode/emacs/vim plugin. People have developed Lean 4 REPLs for example here: https://github.com/arthurpaulino/LeanREPL but using it in an editor will be infinitely more convenient, especially when you start getting into writing interactive proofs.

[banach123]

ok, thanks a lot!

[Kyle Miller]

Things like #eval give you a REPL-like experience when you're using editor plugins:

def f (x : Nat) := 2*x+2

#eval f 10
-- shows 22 in the infoview

[Arthur Paulino]

The REPL implementations are mostly meant to serve as backend for some other applications (like Jupyter notebooks)