Issues

• Missing preFile in example code in Section 6.1.3

  leanprover/fp-lean#304 · Filter by author yak1ex opened on Sep 27, 2026

• Odd page break in chapter on Monads

  leanprover/fp-lean#303 · Filter by author langston-barrett opened on Sep 24, 2026

• minus function in GettingToKnow/DatatypesPatterns.lean doesn't work

  leanprover/fp-lean#301 · Filter by author austinmcdannald opened on Sep 17, 2026

• Publishing the lean introduction book as an epub file

  leanprover/fp-lean#299 · Filter by author martinResearch opened on Aug 31, 2026
  1

• UnusedVariable warning in Point3D pattern matching example (depth function) 1.5.1. Pattern Matching

  leanprover/fp-lean#298 · Filter by author Skynetplus0 opened on Aug 22, 2026

• namespaces Nat.double vs _root_.Nat.double

  leanprover/fp-lean#296 · Filter by author arademaker opened on Aug 13, 2026

• Plus is used instead Add class

  leanprover/fp-lean#291 · Filter by author yaitskov opened on Aug 2, 2026

• building the book for offline reading is broken

  leanprover/fp-lean#283 · Filter by author dimpase opened on Jul 24, 2026
  1

• 3.1.6.3 HTTP Requests

  leanprover/fp-lean#282 · Filter by author alech opened on Jul 13, 2026

• Request: add a chapter or section on lazy evaluation

  leanprover/fp-lean#279 · Filter by author SantiDu opened on Jun 24, 2026

• Section 3: C++ might not be a good example for limitations of overloading

  leanprover/fp-lean#278 · Filter by author GoldsteinE opened on Jun 23, 2026

• §8.3.3 Exercises asks me to implement ForM using for … in in the wrong monad

  leanprover/fp-lean#274 · Filter by author lilyball opened on May 8, 2026

• Accessibility of text in browser

  leanprover/fp-lean#271 · Filter by author pjgoodall opened on Apr 25, 2026
  1

• [Typo] 7.2.2. A Universe of Finite Types: typo in Finite.enumerate .pair explanation

  Typo
  leanprover/fp-lean#269 · Filter by author ilya-fiveisky opened on Apr 11, 2026

• Section 2.1.4. dropRightWhile is deprecated (Combining IO Actions)

  leanprover/fp-lean#267 · Filter by author capistaincap opened on Mar 21, 2026
  1

• Add Run on Lean 4 Playground Button (similar to metaprogramming in lean 4)

  leanprover/fp-lean#266 · Filter by author JadAbouHawili opened on Mar 14, 2026

• Section 5.4: Wrong simplification for checkCompany

  leanprover/fp-lean#265 · Filter by author h-bex opened on Feb 7, 2026

• Fragmented Explanation for Coercion of Nat to Option (Option (Option Nat)) Example

  leanprover/fp-lean#263 · Filter by author JadAbouHawili opened on Jan 28, 2026

• Add Explicit Reference to Definition of idahospiders in 3.5.6 Append Example

  leanprover/fp-lean#262 · Filter by author JadAbouHawili opened on Jan 26, 2026

• [Typo] 3.1.6.1. Another Representation , Type Signature of succ

  Typo
  leanprover/fp-lean#261 · Filter by author JadAbouHawili opened on Jan 21, 2026
  1

• 3.5.3: question about 1 + x in (fun (x : Nat) => 1 + x) = (Nat.succ ·)

  leanprover/fp-lean#260 · Filter by author xuhongxu96 opened on Jan 15, 2026

• Suggestion: Clarify the redundancy in theorem Nat.le_succ_of_le proof

  leanprover/fp-lean#258 · Filter by author FlyCloudC opened on Dec 27, 2025

• In §1.3.2.1 (“Messages You May Meet”)

  leanprover/fp-lean#254 · Filter by author robseau opened on Dec 22, 2025

• Definition of NDBType.asType in exercise 7.3.6.2. Nullable Types

  leanprover/fp-lean#252 · Filter by author whxvd opened on Dec 3, 2025
  1

• [Typo] Misplaced parens in MonadLift for transformers

  Typo
  leanprover/fp-lean#251 · Filter by author david-christiansen opened on Dec 1, 2025
  2