[obsidian] vault backup: 2023-08-30 15:58:42[
This commit is contained in:
parent
e905ecffc2
commit
c7fd29a0f9
7
content/依存型.md
Normal file
7
content/依存型.md
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
#programming-language
|
||||||
|
|
||||||
|
項でインデックス付された型
|
||||||
|
|
||||||
|
C++でいう`decltype(term)`(だよね?)
|
||||||
|
|
||||||
|
[Implementing Dependent Types](https://tiarkrompf.github.io/notes/?/dependent-types/)
|
@ -28,7 +28,7 @@ http://www.cs.tsukuba.ac.jp/~kam/lecture/gairon2-2012/gairon2.pdf
|
|||||||
|
|
||||||
[SATySFi の多段階計算入門](https://sankantsu.hatenablog.com/entry/2022/08/19/215024)
|
[SATySFi の多段階計算入門](https://sankantsu.hatenablog.com/entry/2022/08/19/215024)
|
||||||
|
|
||||||
## 依存型との組み合わせ
|
## [[依存型]]との組み合わせ
|
||||||
|
|
||||||
[A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)
|
[A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user