aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
278 stars 16 forks source link

More Faithful Highlight #1121

Open HoshinoTented opened 3 months ago

HoshinoTented commented 3 months ago

For now, we highlight the desugared concrete syntax which contains the generated code that is NOT the user's code.

However, this is quite difficult since we need to highlight them before desugar, we may need a dedicated ModuleLoader and some code needs to be reorganized.