Skip to content
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.

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

Exercises for Ch.Syntax & Ch.Elaboration #87

Merged
Prev Previous commit
Next Next commit
Ch.Syntax - make list display as a list in .md
lakesare committed Feb 24, 2023
commit 40caf6b51777cd77f41598d9a02d5fe38ba933a7
2 changes: 2 additions & 0 deletions lean/main/syntax.lean
Original file line number Diff line number Diff line change
@@ -220,10 +220,12 @@ syntax "[Bool|" boolean_expr "]" : term
### Syntax combinators
In order to declare more complex syntax, it is often very desirable to have
some basic operations on syntax already built-in, these include:

- helper parsers without syntax categories (i.e. not extendable)
- alternatives
- repetitive parts
- optional parts

While all of these do have an encoding based on syntax categories, this
can make things quite ugly at times, so Lean provides an easier way to do all
of these.