1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79

import Mathlib

/--
Novice Lean programmer
Hey this is kinda like Python right?
-/
def fac₁ n := Id.run do
  let mut ans := 1
  for i in List.range' 1 n do
    ans := ans * i
  return ans

#eval fac₁ 5

/--
Intermediate Lean programmer
Hmmm, just an ordinary functional programming language?
-/
def fac₂ n :=
  if n > 1 then n * fac₂ (n - 1) else n

#eval fac₂ 5

/--
Experienced Lean programmer
It compiles so it's probably correct
-/
def fac₃
  | 0 => 0
  | n + 1 => (n + 1) * fac₃ n

#eval fac₃ 5

/--
Lean golfer
It's so short and cute!
-/
def fac₄ n :=
  [1:n+1].toList.prod

#eval fac₄ 5

/-
Evil Lean programmer
-/
namespace evil
instance : Zero ℕ where
  zero := 1

instance : Add ℕ where
  add := Nat.mul

def fac₅ n :=
  List.range' 1 n |>.sum

#eval fac₅ 5
end evil

/--
Secretly a mathematician
-/
def fac₆ n :=
  ∏ i ∈ Finset.Ioc 0 n, i

#eval fac₆ 5

/--
Openly a mathematician
-/
noncomputable def fac₇ (n : ℕ) : ℂ :=
  ∫ x in Set.Ioi (0 : ℝ), ↑(-x).exp * ↑x ^ n

example : fac₇ 5 = 120 := by
  rw [fac₇]
  suffices Complex.GammaIntegral 6 = 120 by
    rw [← this, Complex.GammaIntegral]
    norm_cast
  rw [← Complex.Gamma_eq_integral (by simp), Complex.Gamma_ofNat_eq_factorial]
  simp [Nat.factorial]