greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge pull request #100 from cjl8zf/cjl8zf-L07or_symm.lean-made-to-make

Browse Source 
Small Typo Fix In L07or_symm.lean
This commit is contained in:
Jon Eugster
2025-09-23 22:57:03 +02:00
committed by GitHub
parent a1375414fa 2f04b8be63
commit 1e99f52a29
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/LessOrEqual/L07or_symm.lean
View File

@@ -47,7 +47,7 @@ But we haven't talked about `or` at all. Here's a run-through.
1) The notation for \"or\" is `∨`. You won't need to type it, but you can 1) The notation for \"or\" is `∨`. You won't need to type it, but you can
type it with `\\or`. type it with `\\or`.
2) If you have an \"or\" statement in the *goal*, then two tactics made 2) If you have an \"or\" statement in the *goal*, then two tactics make
progress: `left` and `right`. But don't choose a direction unless your progress: `left` and `right`. But don't choose a direction unless your
hypotheses guarantee that it's the correct one. hypotheses guarantee that it's the correct one.