依存型

programming-language

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

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

Implementing Dependent Types