lean-tui 1.1.1

Standalone TUI infoview for Lean 4 theorem prover
docs.rs failed to build lean-tui-1.1.1
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.

Lean-TUI

A standalone terminal view that draws the proofs and programs you write in Lean as interactive graphs, next to any editor: Helix, Neovim, Zed, Emacs or VS Code.

Helix with lean-tui following the cursor

Views

The view follows your cursor and picks a display mode for the code under it. See display modes for the details.

Compact Semantic tableau
Compact view Semantic tableau view
Hypotheses and goals before and after each tactic. Every tactic step as a node in a proof tree.
Compact tree Data flow
Compact tree view Data flow view
The proof tree on its side with the active state next to it. Term-style proofs and functional programs, split into sub-states.
Effect flow
Effect flow view
Return values and effects of monadic code.

Quick start

  1. Install lean-tui (a static Linux binary from the releases, or with Cargo) and the Lean-Prism language server. See setup for the steps.

  2. Make lean-prism serve your editor's Lean language server. For Helix, in languages.toml:

    [language-server.lean-prism]
command = "lean-prism"
args = ["serve"]

[[language]]
name = "lean"
language-servers = ["lean-prism"]

  3. Open a Lean file in your editor, run lean-tui in a second terminal, and press space k on a proof in Helix. Lean-TUI tells you what it is waiting for until the first graph arrives.

Documentation

  • Setup: installation, editor configuration, when the view updates, troubleshooting.
  • Usage: follow mode, panes, navigation and colors.
  • Display modes: what each view shows, with examples.
  • Keybindings: every key, generated from the source.

Contributing

Issues and pull requests are welcome. Much of the work happens in the Lean back-end, Lean-Prism, so Lean users who don't write Rust can contribute there. See CONTRIBUTING.md.