e817257922
TODO: `registerParserCategory` uses `registerAttribute` which relies on the environment having a declaration of type `AttributeImpl`. This is bad since forces users to import `Init.Lean`. @Kha The key problem is that we cannot serialize `AttributeImpl`. I will try to address this issue tomorrow. I am considering different workarounds. |
||
|---|---|---|
| .. | ||
| Command.lean | ||
| Identifier.lean | ||
| Level.lean | ||
| Module.lean | ||
| Parser.lean | ||
| Term.lean | ||
| Transform.lean | ||