@mevenlennonbertrand@lipn.info
Post #2649825
2026-05-09 10:05 UTC
@jonmsterling@mathstodon.xyz I think I have a vague idea of what you have in mind. I guess this is related to the LCF-like approach you mentioned for Pterodactyl a while ago? And I guess the big difference with Andromeda 2 is, as you say, that when the TT does not suck you have access to much more meta-theorems/operations via the interface?
I've been thinking about somewhat similar things (although probably not quite) recently, along the lines of "verifying an implementation when you are given only a GAT and its metatheory". This case too should not be extremely hard, but nonetheless interesting.
In any case, happy to chat!
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-05-09 10:36
@mevenlennonbertrand@lipn.info Yes! This is actually inspired by the way I usually implement elaborators. And this approach does indeed work at the level of SOGATs.