Search results

Section 2.1.4. dropRightWhile is deprecated (Combining IO Actions)

Status: Open.

#267 In leanprover/fp-lean;

· capistaincap opened on Mar 21, 2026

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

Status: Open.

#266 In leanprover/fp-lean;

· JadAbouHawili opened on Mar 14, 2026

Section 5.4: Wrong simplification for checkCompany

Status: Open.

#265 In leanprover/fp-lean;

· h-bex opened on Feb 7, 2026

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

Status: Open.

#263 In leanprover/fp-lean;

· JadAbouHawili opened on Jan 28, 2026

Add Explicit Reference to Definition of idahospiders in 3.5.6 Append Example

Status: Open.

#262 In leanprover/fp-lean;

· JadAbouHawili opened on Jan 26, 2026

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

TypoTypographical or grammatical errors in the textTypographical or grammatical errors in the text

Status: Open.

#261 In leanprover/fp-lean;

· JadAbouHawili opened on Jan 21, 2026

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

Status: Open.

#260 In leanprover/fp-lean;

· xuhongxu96 opened on Jan 15, 2026

Suggestion: Clarify the redundancy in theorem Nat.le_succ_of_le proof

Status: Open.

#258 In leanprover/fp-lean;

· FlyCloudC opened on Dec 27, 2025

In §1.3.2.1 (“Messages You May Meet”)

Status: Open.

#254 In leanprover/fp-lean;

· robseau opened on Dec 22, 2025

Definition of NDBType.asType in exercise 7.3.6.2. Nullable Types

Status: Open.

#252 In leanprover/fp-lean;

· whxvd opened on Dec 3, 2025

[Typo] Misplaced parens in MonadLift for transformers

TypoTypographical or grammatical errors in the textTypographical or grammatical errors in the text

Status: Open.

#251 In leanprover/fp-lean;

· david-christiansen opened on Dec 1, 2025

6.3.2. The ManyT exercise seems to be less trivial than intended

Status: Open.

#250 In leanprover/fp-lean;

· whxvd opened on Nov 28, 2025