Post #2103977
2026-02-09 14:45 UTC
@olynch Is your approach based on an inductively defined predicate on types like isStatic? If so, I’m not sure if this would work for this style of erasure where there is a separate sort for erased vs runtime terms, but only one kind of ‘type’. Either way I would be interested to hear more.
Replies (1)
-
@olynch@mathstodon.xyz 2026-02-09 15:00
@constantine Let's chat about it! I have a TYPES submission on my approach, but I still need to do some work before I put confident math statements on the public internet.