#programminglanguage 

項でインデックス付された型

C++でいう`decltype(term)`（だよね？）

[Implementing Dependent Types](https://tiarkrompf.github.io/notes/?/dependent-types/)