leanprover-community/lean4-metaprogramming-book

Issues

• description of `Lean.PrettyPrinter.Delaborator.Delab` is outdated

  #153 opened 13 days ago by Seasawher
  1

• Typo in `MetaM` chapter: the signature of `Lean.commitIfNoEx` is wrong

  #140 opened 17 days ago by spinylobster
  0

• typo in MetaM chapter

  #141 opened 17 days ago by Seasawher
  0

• Pdf should render inline code & unicode symbols

  #100 opened 2 years ago by lakesare
  1

• Add to vscode docview?

  #138 opened 8 months ago by alok
  0

• `let x := v in b` syntax

  #135 opened 10 months ago by Seasawher
  0

• Pdf is not including images from markdown

  #116 opened a year ago by bernborgess
  1

• `#h` does not work

  #133 opened 10 months ago by Seasawher
  0

• Bugs : Typos in `MetaM` chapter

  #132 opened a year ago by Shreyas4991
  0

• Resolve duplication issues in README and SUMMARY

  #126 opened a year ago by Seasawher
  3

• links to md files are broken

  #128 opened a year ago by Seasawher
  5

• Run CI on PRs that come from forks

  #107 opened a year ago by Julian
  0

• put link to html version of book in README

  #64 opened a year ago by kbuzzard
  2

• Add CI for detecting changes to Markdown but not Lean files

  #113 opened a year ago by Julian
  0

• update build command in README

  #124 opened a year ago by Seasawher
  0

• using mdgen instead of lean2md

  #122 opened a year ago by Seasawher
  0

• chapter 9 <;>

  #119 opened a year ago by fpvandoorn
  0

• #assertType 5 : ?_ does in fact result in success

  #101 opened a year ago by jcommelin
  0

• Adding exercises

  #84 opened 2 years ago by lakesare
  1

• Avoid deprecated getMVarDecl etc.

  #68 opened 2 years ago by JLimperg
  0

• metam: use `isImplementationDetail` instead of `isAuxDecl`

  #76 opened 2 years ago by JLimperg
  0

• Change to delayed mvar assignments

  #62 opened 2 years ago by JLimperg
  1

• Introduction chapter: Getting an error on assertTypeCmd in Lean4

  #75 opened 2 years ago by lakesare
  4

• metam: add section on debugging

  #67 opened 2 years ago by JLimperg
  1

• Explain `toExpr` and `toTypeExpr`

  #73 opened 2 years ago by arthurpaulino
  0

• Iterate on feedback from Dan

  #40 opened 3 years ago by arthurpaulino
  1

• unexpanders should not match on the constant's name

  #72 opened 2 years ago by javra
  0

• metam: add note about matching expressions with `isDefEq`

  #70 opened 2 years ago by JLimperg
  0

• metam: add section on type checking, type inference, typeclass inference

  #69 opened 2 years ago by JLimperg
  0

• `and_then` is subtly different from `<;>`. The former focuses the goal, whereas the latter does not.

  #49 opened 3 years ago by alexkeizer
  3

• Clarity for Tactic chapter

  #61 opened 3 years ago by winston-h-zhang
  0

• Iterate on feedback from Patrick

  #39 opened 3 years ago by arthurpaulino
  1

• can you make the introductory version of Lean4, i cant find one.

  #54 opened 3 years ago by rizkidotme
  2

• `md` parameter of `whnf'` is unused

  #55 opened 3 years ago by dwrensha
  2

• Iterate on feedback by Alex

  #47 opened 3 years ago by hargoniX
  0

• Iterate on feedback from Sebastian

  #38 opened 3 years ago by arthurpaulino
  0

• Divide the DSL chapter in subsections

  #37 opened 3 years ago by arthurpaulino
  0

• Add the book structure (prerequisites) in the intro chapter

  #41 opened 3 years ago by arthurpaulino
  0

• `mkAppN` vs `mkAppM`

  #36 opened 3 years ago by arthurpaulino
  0

• Cover matching on expressions

  #29 opened 3 years ago by arthurpaulino
  0