Post #2103976
2026-02-09 14:21 UTC
@constantine
> primitive modality, which cannot be done with SOGATs
OK good, I still have some tricks you haven't figured out 😜
Replies (1)
-
@constantine@types.pl 2026-02-09 14:45
@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.