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

26 Open 13 Closed
26 Open 13 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

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
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
1
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
ambiguous, possible interpretations on sample code in Quantifiers and Equality chapter
#111 opened Apr 21, 2024 by trj2059
Some graphics missing in VSCodium
#109 opened Mar 16, 2024 by navidrashidian
2
The theme changes when I click on the print icon
#105 opened Feb 23, 2024 by xiaoxi-david
auto bound implicit args are not limited to single letters
#100 opened Feb 3, 2024 by medovina
@david-christiansen
1
Make keywords searchable
#86 opened Dec 3, 2023 by BoltonBailey
suffices: multiple goals not appearing as the text suggests?
#82 opened Oct 23, 2023 by dijkstracula
check that comments agree with hovers
#72 opened Jul 15, 2023 by erniecohen
Page not found
#71 opened Jul 4, 2023 by dataopt
1
noConfusion and unreachable patterns
#58 opened Feb 13, 2023 by rambip
1
Maybe it is worth emphasizing that Proof is not a built-in type
#57 opened Feb 8, 2023 by zxch3n
1
Anonymous constructor notation
#29 opened Feb 18, 2022 by ydewit
1
Broken link
#28 opened Feb 12, 2022 by arademaker
2
1
ProTip! Exclude everything labeled bug with -label:bug.