Skip to content

Issues: leanprover/theorem_proving_in_lean4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

38 Open 12 Closed
38 Open 12 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

nat_lit example no longer needs nat_lit
#152 opened Feb 18, 2025 by rkirov
new type class syntax used without introduction
#151 opened Feb 18, 2025 by rkirov
1
simp contextual example in Tactics chapter
#150 opened Jan 28, 2025 by MrQubo
1
Copying doesn't include context in Tactics chapter
#149 opened Jan 28, 2025 by MrQubo
Broken proof in Induction & Recursion -> Local Recursive Decls
#148 opened Jan 18, 2025 by ketilwright
Possible typo in chapter 8 -> dependent pattern matching
#147 opened Jan 18, 2025 by ketilwright
link with hashtag do not scroll to correct position
#146 opened Dec 29, 2024 by zqc17
True.intro is of type True, no true
#145 opened Dec 23, 2024 by jcvillaquira
#eval natToBin 123456 should be #eval!
#140 opened Nov 24, 2024 by ketilwright
Broken div example proof chapter 8
#139 opened Nov 24, 2024 by ketilwright
Broken length_replicate proof (chapter 8)
#138 opened Nov 23, 2024 by ketilwright
1
Explanation of what a structure is
#137 opened Nov 2, 2024 by hrmacbeth
Error in 2nd subst example
#136 opened Oct 31, 2024 by ketilwright
recursion depth problem in chapter 7 examples
#134 opened Oct 30, 2024 by ketilwright
3
mutual is not highlighted
#132 opened Oct 22, 2024 by seanmcl
Error "unknown identifier 'hp'" in chapter 3 "Propositions and Proofs" when using variable (hp: p)
#131 opened Oct 20, 2024 by MichaelJFishman
4
Hypotheses as variables not available in theorems with lean 4.12
#130 opened Oct 8, 2024 by ketilwright
4
PDF version
#129 opened Sep 21, 2024 by projetmbc
Ch. 6 "Using the Library" link broken
#127 opened Aug 28, 2024 by Morgan-Sinclaire
These 2 sentences in Ch. 7 are a holdover from Lean3
#126 opened Aug 26, 2024 by Morgan-Sinclaire
This should be capital True I think
#125 opened Aug 6, 2024 by johnmwu
compound repeat first tactic no longer solves all three permutations of \and propositions
#121 opened Jul 7, 2024 by jordane95
Examples in Inductive Types chapter broken due to simp_eq_add_one simp rule
#120 opened Jun 23, 2024 by avigad
Propositions and currying
#116 opened May 26, 2024 by DavidPratten
Duplicate section on Local recursive declarations
#115 opened May 8, 2024 by solleks
ProTip! no:milestone will show everything without a milestone.