Skip to content

Commit

Permalink
remove "if I've written it" comment because I now have
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Dec 22, 2023
1 parent 9815f76 commit b893d5f
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Game/Levels/LessOrEqual/L11le_two.lean
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,6 @@ Nice!
The next step in the development of order theory is to develop
the theory of the interplay between `≤` and multiplication.
If you've already done Multiplication World, step into
Advanced Multiplication World (once I've written it...)
If you've already done Multiplication World, you're now ready for
Advanced Multiplication World. Click on \"Leave World\" to access it.
"

0 comments on commit b893d5f

Please sign in to comment.