quartz-research-note/content/依存型.md

#programming-language 

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

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

[Implementing Dependent Types](https://tiarkrompf.github.io/notes/?/dependent-types/)
[obsidian] vault backup: 2023-12-06 20:20:54[ 2023-12-06 11:20:54 +00:00			`#programming-language`
[obsidian] vault backup: 2023-08-30 15:58:42[ 2023-08-30 06:58:42 +00:00
			`項でインデックス付された型`

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

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