diff --git a/README.md b/README.md index 963ef97..f0f436e 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,10 @@ This builds the executable in `.lake/build/bin/pantograph-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