In Lean4, several builtin operators will be defined programmatically to make sure we can bootstrap the system before we have all primitives necessary for defining parsers. |
||
|---|---|---|
| .. | ||
| default.lean | ||
| identifier.lean | ||
| level.lean | ||
| parser.lean | ||
| term.lean | ||
| trie.lean | ||