issues
search
leanprover-community
/
lean4-metaprogramming-book
https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204
stars
47
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Fix typos
#92
pitmonticone
closed
1 year ago
1
Better intro for Expressions chapter
#91
JLimperg
closed
1 year ago
0
Quick fixes for pdf lists to render fine
#90
lakesare
closed
1 year ago
0
Update syntax.md
#89
yangky11
closed
1 year ago
2
fix typo
#88
kbuzzard
closed
1 year ago
0
Exercises for Ch.Syntax & Ch.Elaboration
#87
lakesare
closed
1 year ago
2
Enable pdf generation in prs; fix chapter structure
#86
lakesare
closed
1 year ago
1
Adding exercises
#85
lakesare
closed
1 year ago
9
Adding exercises
#84
lakesare
opened
1 year ago
1
Update Lean to nightly-2022-12-16
#83
JLimperg
closed
1 year ago
0
expressions: clarify bvar/fvar terminology
#82
JLimperg
closed
1 year ago
0
lint(lean/main/tactics): remove unused definition
#81
adomani
closed
1 year ago
0
typos(lean/main/tactics.lean): some typos
#80
adomani
closed
1 year ago
3
questions(lean/main/tactics.lean)
#79
adomani
closed
1 year ago
3
expressions: add section about universe levels
#78
JLimperg
closed
1 year ago
2
Clean up some deprecations etc.
#77
JLimperg
closed
1 year ago
1
metam: use `isImplementationDetail` instead of `isAuxDecl`
#76
JLimperg
closed
1 year ago
0
Introduction chapter: Getting an error on assertTypeCmd in Lean4
#75
lakesare
closed
1 year ago
4
fix a typo in intro.md
#74
jcommelin
closed
1 year ago
1
Explain `toExpr` and `toTypeExpr`
#73
arthurpaulino
opened
1 year ago
0
unexpanders should not match on the constant's name
#72
javra
opened
1 year ago
0
[Draft] Simple attributes
#71
bollu
opened
1 year ago
0
metam: add note about matching expressions with `isDefEq`
#70
JLimperg
opened
1 year ago
0
metam: add section on type checking, type inference, typeclass inference
#69
JLimperg
opened
1 year ago
0
Avoid deprecated getMVarDecl etc.
#68
JLimperg
closed
1 year ago
0
metam: add section on debugging
#67
JLimperg
opened
2 years ago
1
Dev
#66
arthurpaulino
closed
2 years ago
0
Macro for `\mapsTo` in introduction
#65
siddhartha-gadgil
closed
2 years ago
0
put link to html version of book in README
#64
kbuzzard
closed
6 months ago
2
fix: 't <|> u' -> 'first | t | u'
#63
dwrensha
closed
2 years ago
0
Change to delayed mvar assignments
#62
JLimperg
closed
1 year ago
1
Clarity for Tactic chapter
#61
winston-h-zhang
opened
2 years ago
0
Update to Lean nightly-2022-07-06
#60
JLimperg
closed
2 years ago
1
metam: add section about MonadBacktrack
#59
JLimperg
closed
2 years ago
0
Update to latest Lean
#58
hargoniX
closed
2 years ago
0
metam: extend sections on (de)constructing Exprs
#57
JLimperg
closed
2 years ago
1
remove unused parameter from whnf'
#56
dwrensha
closed
2 years ago
0
`md` parameter of `whnf'` is unused
#55
dwrensha
closed
2 years ago
2
can you make the introductory version of Lean4, i cant find one.
#54
rizkidotme
closed
2 years ago
2
feat: more on syntax quotations and hygiene
#53
hargoniX
closed
2 years ago
0
metam: expand discussion of metavariables
#52
JLimperg
closed
2 years ago
0
metam: fix wrong explanation of WHNF
#51
JLimperg
closed
2 years ago
2
`metam.lean`: minor fixes/clarifications
#50
rish987
closed
2 years ago
0
`and_then` is subtly different from `<;>`. The former focuses the goal, whereas the latter does not.
#49
alexkeizer
opened
2 years ago
3
`syntax.lean`: minor details and typo/grammar/punctuation fixes
#48
rish987
closed
2 years ago
0
Iterate on feedback by Alex
#47
hargoniX
closed
2 years ago
0
manual new line in markdown
#46
siddhartha-gadgil
closed
2 years ago
0
Tweak the PDF build a bit
#45
Julian
closed
2 years ago
2
Blank lines before markdown list to fix formatting
#44
siddhartha-gadgil
closed
2 years ago
0
addressing Sebastian's comments
#43
arthurpaulino
closed
2 years ago
0
Previous
Next