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

#programminglanguage 

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

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

[Implementing Dependent Types](https://tiarkrompf.github.io/notes/?/dependent-types/)
[obsidian] vault backup: 2023-09-12 17:58:02[ 2023-09-12 08:58:02 +00:00			`#programminglanguage`
[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/)`