From e8fdd906aaf807a3132bffea67cbe14bbf4e8e6c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 20:09:54 -0700 Subject: [PATCH] doc: Remove stale documentation --- README.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 963ef97..7e1e416 100644 --- a/README.md +++ b/README.md @@ -17,17 +17,21 @@ nix build .#{sharedLib,executable} ``` to build either the shared library or executable. -Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and -run +For non-Nix users, install `lake` and `lean` fixed to the version of the +`lean-toolchain` file, and run ``` sh lake build ``` -This builds the executable in `.lake/build/bin/pantograph-repl`. +This builds the executable in `.lake/build/bin/repl`. ### Executable Usage -See [Executable Usage](./doc/repl.md) +The default build target is a Read-Eval-Print-Loop (REPL). See [REPL +Documentation](./doc/repl.md) + +Another executable is the `tomograph`, which processes a Lean file and displays +syntax or elaboration level data. ### Library Usage @@ -39,7 +43,7 @@ Inject any project path via the `pantograph_init_search` function. ## Development -A Lean development shell is provided in the Nix flake. +A Lean development shell is provided in the Nix flake. Nix usage is optional. ### Testing