@ncf Mm given that the syntax and whatever "extra work" the checker does is also all implemented in Lean, that just about boils down to the content of my first paragraph with extra steps, no? Unless I misunderstood something about the setup. But I also cba trying to further make precise what the creators cba to properly document.

@mildsunrise