iskm/learnxinyminutes-docs
1
0
Fork 0
mirror of https://github.com/adambard/learnxinyminutes-docs.git synced 2024-12-23 17:41:41 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[lean/en] add space before colon (#5132)
Some checks failed
Trigger site build / deploy (push) Has been cancelled
Details
CI / lint (push) Has been cancelled
Details

Browse Source
This commit is contained in:
Martin Dvořák 2024-10-04 01:50:47 +02:00 committed by GitHub
parent fa0e3c632f
commit 90d544271e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lean4.html.markdown
View File

@ -256,7 +256,7 @@ We now state Collatz conjecture. The proof is left as an exercise to the reader.
def collatz_next (n : Nat) : Nat := def collatz_next (n : Nat) : Nat :=
if n % 2 = 0 then n / 2 else 3 * n + 1 if n % 2 = 0 then n / 2 else 3 * n + 1
def iter (k : Nat) (f: Nat → Nat) := def iter (k : Nat) (f : Nat → Nat) :=
match k with match k with
| Nat.zero => fun x => x | Nat.zero => fun x => x
| Nat.succ k' => fun x => f (iter k' f x) | Nat.succ k' => fun x => f (iter k' f x)