Skip to content

Issues: leanprover-community/lean4-metaprogramming-book

Beta
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

18 Open 24 Closed
18 Open 24 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

Introduction chapter: #assertType example likely not behaving as expected in Lean 4.17
#168 opened Mar 9, 2025 by philnguyen
Tactic chapter/FAQ: add creation of a fresh unique name
#166 opened Mar 4, 2025 by bodoai
description of Lean.PrettyPrinter.Delaborator.Delab is outdated
#153 opened Dec 29, 2024 by Seasawher
1
Add to vscode docview?
#138 opened May 2, 2024 by alok
let x := v in b syntax
#135 opened Mar 23, 2024 by Seasawher
Bugs : Typos in MetaM chapter
#132 opened Feb 19, 2024 by Shreyas4991
chapter 9 <;>
#119 opened Dec 7, 2023 by fpvandoorn
Pdf is not including images from markdown
#116 opened Oct 27, 2023 by bernborgess
1
1
Pdf should render inline code & unicode symbols
#100 opened Jun 22, 2023 by lakesare
1
Adding exercises
#84 opened Jan 2, 2023 by lakesare
9 of 13 tasks
1
Explain toExpr and toTypeExpr
#73 opened Aug 22, 2022 by arthurpaulino
unexpanders should not match on the constant's name
#72 opened Jul 28, 2022 by javra
metam: add note about matching expressions with isDefEq
#70 opened Jul 26, 2022 by JLimperg
metam: add section on type checking, type inference, typeclass inference
#69 opened Jul 26, 2022 by JLimperg
metam: add section on debugging
#67 opened Jul 21, 2022 by JLimperg
1
Clarity for Tactic chapter
#61 opened Jul 10, 2022 by winston-h-zhang
and_then is subtly different from <;>. The former focuses the goal, whereas the latter does not.
#49 opened Jun 14, 2022 by alexkeizer
3
Iterate on feedback from Dan
#40 opened Jun 12, 2022 by arthurpaulino
1
ProTip! no:milestone will show everything without a milestone.