From c7fd29a0f9e58445b0450a90ea6de6aae0f801c8 Mon Sep 17 00:00:00 2001 From: "Tomoya(obsidian)" Date: Wed, 30 Aug 2023 15:58:42 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-08-30 15:58:42[ --- content/依存型.md | 7 +++++++ content/多段階計算.md | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 content/依存型.md 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)