Commit 2020-10-09 13:16 fcaf6e91
View on Github →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.
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.