Skip to content

Commit

Permalink
fix typo #44
Browse files Browse the repository at this point in the history
  • Loading branch information
@joneugster
joneugster committed Nov 29, 2023
1 parent d61fe73 commit 14f19a4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Game/Levels/LessOrEqual/L04le_trans.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ and $Q\\implies R$.
"

Introduction "
In this level, we inequalities as *hypotheses*. We have not seen this before.
In this level, we see inequalities as *hypotheses*. We have not seen this before.
The `cases` tactic can be used to take `hxy` apart.
"

Expand Down

0 comments on commit 14f19a4

Please sign in to comment.