Skip to content

Commit

Permalink
Merge pull request #49 from pitmonticone/main
Browse files Browse the repository at this point in the history
Fix typo in Definitions.lean
  • Loading branch information
joneugster authored Feb 2, 2024
2 parents d24f07d + c8f7f2c commit b922d89
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Game/Doc/Definitions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ import GameServer.Commands

-- * `(0 : ℕ)`, an element called zero.
-- * `(succ : ℕ → ℕ)`, the successor function , i.e. one is `succ 0` and two is `succ (succ 0)`.
-- * `induction` (or `rcases`), tactics to treat the cases $n = 0$ and `n = m + 1` seperately.
-- * `induction` (or `rcases`), tactics to treat the cases $n = 0$ and `n = m + 1` separately.

-- ## Game Modifications

Expand Down

0 comments on commit b922d89

Please sign in to comment.