From ef9c255f5815cfac372eeb41e5e0466e66c818ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?= =?UTF-8?q?a?= Date: Thu, 7 Dec 2023 17:36:32 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-12-07 17:36:31[ --- content/多段階計算.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/content/多段階計算.md b/content/多段階計算.md index 72715626..9edaaf8b 100644 --- a/content/多段階計算.md +++ b/content/多段階計算.md @@ -43,4 +43,11 @@ https://link.springer.com/chapter/10.1007/978-3-030-34175-6_4 > Our goal is to define the function `vadd` of type $$Πn : Int.∀β.⊲β(Vector (\%_αn) → Vector (\%_αn) → Vector (\%_αn))$$ > .It takes the length n and returns (β-closed) code of a function to add two vectors of length n. The generated code is run by applying it to ε to obtain a function of type $Vector\; n → Vector\; n → Vector\; n$ as expected. -この辺はなんかやりたいことに近そうな予感がする \ No newline at end of file +この辺はなんかやりたいことに近そうな予感がする + + +## [[Rust]]でのプログラム合成 + +https://fitzgeraldnick.com/2018/11/15/program-synthesis-is-possible-in-rust.html + +impl Return typeと組み合わせたらもっと派手なことできそう \ No newline at end of file