leanprover-community/repl

This is stars and forks stats for /leanprover-community/repl repository. As of 05 May, 2024 this repository has 24 stars and 3 forks.

A read-eval-print-loop for Lean 4 Run using lake exe repl. Communicates via JSON on stdin and stdout. Commands should be separated by blank lines. The REPL works both in "command" mode and "tactic" mode. Command mode In command mode, you send complete commands (e.g. declarations) to the REPL. Commands may be of the form { "cmd" : "def f := 2" } { "cmd" : "example : f = 2 := rfl", "env" : 1 } The env field, if present, must contain a number received in the env field of a previous response, and causes...