mathlib3
fcaf6e91
- feat(meta/expr): add parser for generated binder names (#4540)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
feat(meta/expr): add parser for generated binder names (#4540) During elaboration, Lean generates a name for anonymous Π binders. This commit adds a parser that recognises such names.
References
#4925 - Make prime-avoidance branch build
Author
JLimperg
Parents
306dc8a0
Loading