@mevenlennonbertrand@lipn.info
Post #2649823
2026-05-08 13:55 UTC
@jonmsterling@mathstodon.xyz Can you say a little bit more about what you have in mind with your first point? I'm definitely curious/interested!
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-05-08 14:21
@mevenlennonbertrand@lipn.info Happy to chat more about this. Roughly the idea is that it’s (1) correct by construction, (2) isolates where all the important syntactic-metatheory results need to be used, (3) completely abstracted from core-syntax and the method used to check equality or invert heads, (4) and the mathematical elaboration definition looks a lot like the Haskell/OCaml code of an elaborator. The "hard" version that I alluded to also works when the metatheory sucks or isn't yet developed (e.g. like Andromeda etc.).