phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Typo in documentation, hints.md

Browse Source
This commit is contained in:
JadAbouHawili
2024-05-02 17:38:30 +00:00
committed by GitHub
parent d034148bec
commit 18f21fa324
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/hints.md
+1 -1
View File
@@ -33,7 +33,7 @@ You can use `Branch` to place hints
in dead ends or alternative proof strands. in dead ends or alternative proof strands.
A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
so that no progress has been made on proofing the goal. so that no progress has been made on proving the goal.
``` ```
Statement .... := by Statement .... := by