From 76ee7cfce5c82214022c9a46af3a252c2a8b0cca Mon Sep 17 00:00:00 2001 From: "Tomoya Matsuura(MacBookPro)" Date: Fri, 25 Aug 2023 18:44:49 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-08-25 18:44:49[ --- content/Coqの勉強.md | 1 + 1 file changed, 1 insertion(+) diff --git a/content/Coqの勉強.md b/content/Coqの勉強.md index 38bbab5a..7d21823e 100644 --- a/content/Coqの勉強.md +++ b/content/Coqの勉強.md @@ -9,6 +9,7 @@ - 千葉大学大学院 [定理証明支援系 Coq での 論理的なリーゾニング 集中講義 アフェルト レナルド(2017)](https://staff.aist.go.jp/reynald.affeldt/coq/riron.pdf) - IIJ技術研究所 [Coq を始めよう 池渕未来(2011)](https://www.iijlab.net/activities/programming-coq/coqt1.html) - [Real World Coq – An introduction to effective theorem proving](https://ejgallego.github.io/real-world-coq/) by [[Emilio Jesús Gallego Arias]] + - jsCoqを使ってインタラクティブに学べる（DeepLとかのブラウザ拡張でレイアウトが崩れるっぽい） ## 備忘録 - `Inductive`が変数宣言