leanprover/fp-lean

View on GitHub

Functional Programming in Lean

Stars: 192
Forks: 73
Open beginner issues: 23
Indexed issues: 75

Dominant language: Lean
License: No license data
Last GitHub push: Aug 13, 2026
Latest indexed: Sep 20, 2026
Contributing guide: Contributing guide
Code of conduct: No code of conduct
Beginner labels: No beginner labels indexed
PR merge metrics: No merged PRs in 30d

Beginner friendly Everything

Open All

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

Difficulty 1/5 Under an hour Newbie friendliness 92/100

leanprover/fp-lean#301 · Opened Sep 17, 2026
Publishing the lean introduction book as an epub file Open

Difficulty 3/5 1-2 days Newbie friendliness 58/100

leanprover/fp-lean#299 · 1 comment · Opened Aug 31, 2026
UnusedVariable warning in Point3D pattern matching example (depth function) 1.5.1. Pattern Matching Open

Difficulty 1/5 Under an hour Newbie friendliness 90/100

leanprover/fp-lean#298 · Opened Aug 22, 2026
namespaces `Nat.double` vs `_root_.Nat.double` Open

Difficulty 1/5 Under an hour Newbie friendliness 78/100

leanprover/fp-lean#296 · Opened Aug 13, 2026
Plus is used instead Add class Open

Difficulty 1/5 Under an hour Newbie friendliness 90/100

leanprover/fp-lean#291 · Opened Aug 2, 2026
building the book for offline reading is broken Open

Difficulty 3/5 1-2 days Newbie friendliness 52/100

leanprover/fp-lean#283 · 1 comment · Opened Jul 24, 2026
3.1.6.3 HTTP Requests Open

Difficulty 1/5 Under an hour Newbie friendliness 72/100

leanprover/fp-lean#282 · Opened Jul 13, 2026
Request: add a chapter or section on lazy evaluation Open

Difficulty 4/5 3-5 days Newbie friendliness 45/100

leanprover/fp-lean#279 · Opened Jun 24, 2026
Section 3: C++ might not be a good example for limitations of overloading Open

Difficulty 3/5 1-2 days Newbie friendliness 55/100

leanprover/fp-lean#278 · Opened Jun 23, 2026
§8.3.3 Exercises asks me to implement ForM using `for … in` in the wrong monad Open

Difficulty 1/5 Under an hour Newbie friendliness 78/100

leanprover/fp-lean#274 · Opened May 8, 2026
Accessibility of text in browser Open

Difficulty 3/5 1-2 days Newbie friendliness 45/100

leanprover/fp-lean#271 · 1 comment · Opened Apr 25, 2026
[Typo] 7.2.2. A Universe of Finite Types: typo in Finite.enumerate .pair explanation Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 90/100

leanprover/fp-lean#269 · Opened Apr 11, 2026
Section 2.1.4. `dropRightWhile` is deprecated (Combining IO Actions) Open

Difficulty 1/5 Under an hour Newbie friendliness 48/100

leanprover/fp-lean#267 · 1 comment · 1 reaction · Opened Mar 21, 2026
Add Run on Lean 4 Playground Button (similar to metaprogramming in lean 4) Open

Difficulty 5/5 Over a week Newbie friendliness 25/100

leanprover/fp-lean#266 · Opened Mar 14, 2026
Section 5.4: Wrong simplification for checkCompany Open

Difficulty 2/5 1-3 hours Newbie friendliness 45/100

leanprover/fp-lean#265 · Opened Feb 7, 2026
Fragmented Explanation for Coercion of `Nat to Option (Option (Option Nat))` Example Open

Difficulty 3/5 1-2 days Newbie friendliness 52/100

leanprover/fp-lean#263 · Opened Jan 28, 2026
Add Explicit Reference to Definition of `idahospiders` in 3.5.6 Append Example Open

Difficulty 1/5 Under an hour Newbie friendliness 75/100

leanprover/fp-lean#262 · Opened Jan 26, 2026
[Typo] 3.1.6.1. Another Representation , Type Signature of `succ` Open

Typo

Difficulty 2/5 1-3 hours Newbie friendliness 45/100

leanprover/fp-lean#261 · 1 comment · Opened Jan 21, 2026
3.5.3: question about `1 + x` in `(fun (x : Nat) => 1 + x) = (Nat.succ ·)` Open

Difficulty 2/5 1-3 hours Newbie friendliness 45/100

leanprover/fp-lean#260 · Opened Jan 15, 2026
Suggestion: Clarify the redundancy in theorem `Nat.le_succ_of_le` proof Open

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#258 · Opened Dec 27, 2025
In §1.3.2.1 (“Messages You May Meet”) Open

Difficulty 1/5 Under an hour Newbie friendliness 68/100

leanprover/fp-lean#254 · Opened Dec 22, 2025
Definition of `NDBType.asType` in exercise 7.3.6.2. Nullable Types Open

Difficulty 2/5 1-3 hours Newbie friendliness 63/100

leanprover/fp-lean#252 · 1 comment · 3 reactions · Opened Dec 3, 2025
[Typo] Misplaced parens in MonadLift for transformers Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 48/100

leanprover/fp-lean#251 · 1 comment · Opened Dec 1, 2025
6.3.2. The `ManyT` exercise seems to be less trivial than intended Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/fp-lean#250 · 1 reaction · Opened Nov 28, 2025
[Typo] 8.3.3. Exercises, array reversal Open

Typo

Difficulty 2/5 1-3 hours Newbie friendliness 65/100

leanprover/fp-lean#248 · 2 comments · Opened Nov 22, 2025
`Many` could be more lazy Open

Difficulty 2/5 1-3 hours Newbie friendliness 55/100

leanprover/fp-lean#247 · 1 reaction · Opened Nov 20, 2025
[Typo] Chapter 7.3. `bEq` and `beq` Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 65/100

leanprover/fp-lean#246 · Opened Nov 20, 2025
[Typo] 8.6.4. Is This Really Insertion Sort?: results them -> results in them Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#245 · Opened Nov 17, 2025
[Typo] 8.6.2.1. Termination: two -> to Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 55/100

leanprover/fp-lean#244 · Opened Nov 17, 2025
[Typo] 8.3.2. Proving Termination: as quite as -> quite as Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 68/100

leanprover/fp-lean#243 · Opened Nov 17, 2025
[Typo] 8.3.1.2. Inequality of Natural Numbers: k vs. m Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 55/100

leanprover/fp-lean#242 · Opened Nov 17, 2025
[Typo] Interlude / The Induction Tactic: corresponds the -> corresponds to the Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 72/100

leanprover/fp-lean#241 · Opened Nov 11, 2025
[Typo] 7.5.2. Getting Stuck on Addition: an type mismatch -> a type mismatch Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 92/100

leanprover/fp-lean#240 · Opened Nov 11, 2025
[Typo] 7.2.2. A Universe of Finite Types: wrong indentation Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#239 · Opened Nov 11, 2025
[Typo] 6.6.2. Type Classes for Effects: to a the -> to the Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 65/100

leanprover/fp-lean#238 · Opened Nov 11, 2025
[Typo] 6.1.2. Using a Custom Monad: catch it if -> catch if Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 65/100

leanprover/fp-lean#237 · Opened Nov 11, 2025
[Typo] 6. Monad Transformers: build -> built Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 88/100

leanprover/fp-lean#236 · Opened Nov 11, 2025
[Typo] 5.5. Universes: Y is a X -> X is a Y Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#235 · Opened Nov 11, 2025
[Typo] Section 4.3.3.3. Custom Environments: is a a -> is a Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#234 · Opened Nov 11, 2025
Suggestion: Elaborate more in part 3.2 Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/fp-lean#226 · 1 comment · Opened Oct 6, 2025
Combining IO and Reader uses String.separate instead of String.intercalate Open

Difficulty 1/5 Under an hour Newbie friendliness 55/100

leanprover/fp-lean#202 · Opened Jun 11, 2025
Add information about inlay hints to 1.7.1 Open

Difficulty 1/5 Under an hour Newbie friendliness 35/100

leanprover/fp-lean#199 · Opened Jun 5, 2025
Update build instructions in `README.md` Open

Difficulty 1/5 Under an hour Newbie friendliness 78/100

leanprover/fp-lean#197 · 3 reactions · Opened Jun 4, 2025
Best way to get a PDF version of Functional Programming in Lean? Open

Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/fp-lean#192 · 13 comments · 4 reactions · Opened Jun 3, 2025
`lake exe fp-lean` fails with `bash: doug: command not found` and `Non-zero exit code from 'sort --shared < test-data'` Open

Difficulty 4/5 3-5 days Newbie friendliness 30/100

leanprover/fp-lean#191 · 3 comments · Opened Jun 3, 2025
`deriving Repr` no longer required for structures? Open

Difficulty 2/5 1-3 hours Newbie friendliness 45/100

leanprover/fp-lean#180 · Opened Feb 12, 2025
Suggestion: more thorough summary of function definition alternatives Open

Difficulty 3/5 1-2 days Newbie friendliness 38/100

leanprover/fp-lean#177 · 3 comments · Opened Dec 5, 2024
[Typo] Sect 5.0 "The numbering of the Python equivalent of aTree is" Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#175 · 1 reaction · Opened Nov 29, 2024
[Typo] Sect 5.0, "Logging" section, minor typo "nodes" should be "node" Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 55/100

leanprover/fp-lean#174 · 1 comment · Opened Nov 28, 2024
[Typo] Sect 9 exercise error: "'List.append_assoc' has already been declared" Open

Typo

Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/fp-lean#172 · 1 reaction · Opened Nov 19, 2024

leanprover/fp-lean

Get new issues in your inbox