diff --git a/content/依存型.md b/content/依存型.md new file mode 100644 index 00000000..67b46081 --- /dev/null +++ b/content/依存型.md @@ -0,0 +1,7 @@ +#programming-language + +項でインデックス付された型 + +C++でいう`decltype(term)`(だよね?) + +[Implementing Dependent Types](https://tiarkrompf.github.io/notes/?/dependent-types/) \ No newline at end of file diff --git a/content/多段階計算.md b/content/多段階計算.md index a70048ee..60dee313 100644 --- a/content/多段階計算.md +++ b/content/多段階計算.md @@ -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) -## 依存型との組み合わせ +## [[依存型]]との組み合わせ [A Dependently Typed Multi-Stage Calculus](https://arxiv.org/abs/1908.02035)