55626ba60d
We are going to start making drastic changes in the parser, elaborator, attributes, etc. Examples: - No View objects. I am going to implement match_syntax. - No RecT in the parser. I am going to implement parser extensions using an approach similar to the one I used to implement environment extensions. - No Parsec. I will use an approach similar to the one used in the experiment https://github.com/leanprover/lean4/tree/master/tests/playground/parser It is easier to perform these changes with the new frontend disabled. I will slowly re-active it as I apply the changes. cc @kha |
||
|---|---|---|
| .. | ||
| init | ||
| leanpkg.path | ||
| library.md | ||
| Makefile.in | ||
| relative.py | ||