mention tactic state in README (#63)

* mention tactic state in README * PR suggested edits * Update README.md Co-authored-by: Richard Copley <[email protected]> --------- Co-authored-by: Richard Copley <[email protected]>
leanprover-community · Apr 30, 2024 · 60d066f · 60d066f
1 parent 2eccb30
commit 60d066f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -56,6 +56,8 @@ the word ``#check`` will be underlined, and hovering over it will show
 you the type of ``id``. The mode line will show ``FlyC:0/1``, indicating
 that there are no errors and one piece of information displayed.
 
+To view the proof state, run `lean4-toggle-info` (`C-c` `C-i`). This will show the `*Lean Goals*` buffer (like the `Lean infoview` pane in VSCode) in a separate window.
+
 Settings
 ========