Limitations of indexed types that are not truly dependent

Published: Jan. 14, 2020, noon

b'

If indices to types come from a different syntactic category than programs, there are a few things you cannot do.\\xa0 Some initial thoughts on how to work around these.

'