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

Update Definitions.lean

Browse Source
This commit is contained in:
Pietro Monticone
2024-01-31 12:26:17 +01:00
parent bc38caf177
commit c8f7f2caaa
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Doc/Definitions.lean
View File

@@ -6,7 +6,7 @@ import GameServer.Commands
-- * `(0 : ℕ)`, an element called zero. -- * `(0 : ℕ)`, an element called zero.
-- * `(succ : ℕ → ℕ)`, the successor function , i.e. one is `succ 0` and two is `succ (succ 0)`. -- * `(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 -- ## Game Modifications