Skip to content

Commit

Permalink
cleanup README
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Mar 14, 2024
1 parent 7767705 commit 2ab7948
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ showing any messages generated, and sorries with their goal states.

There is a simple wrapper around command mode that allows reading in an entire file.

If `file.lean` contains
If `test/file.lean` contains
```lean
def f : Nat := 37
Expand All @@ -70,11 +70,11 @@ def g := 2
theorem h : f + g = 39 := by exact rfl
```

then sending
```json
{"path": "test/file.lean", "allTactics": true}
then
```
echo '{"path": "test/file.lean", "allTactics": true}' | lake exe repl
```
to the REPL results in output
results in output
```json
{"tactics":
[{"tactic": "exact rfl",
Expand Down

0 comments on commit 2ab7948

Please sign in to comment.