Lean4 manages to pull off changing the parser on the fly at compile time. You can add new productions, add new syntax node types, and add new tokens. Then defin

Lean4 manages to pull off changing the parser on the fly at compile time. You can add new productions, add new syntax node types, and add new tokens. Then define macros or code to process the additional syntax. Here is a sample I found that adds a simple JSX-like syntax starting around line 93 and then uses it at line 169: https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/Webserver.lean#L93 https://github.com/leanprover/lean4/blob/master/tests/playgr... I believe most of the language is defined this way, although it is pre-compiled. For more details see the lean4 metaprogramming book: https://github.com/arthurpaulino/lean4-metaprogramming-book https://github.com/arthurpaulino/lean4-metaprogramming-book