この論文、参考になる。 https://kwarc.info/people/frabe/Research/KRW_isabelle_19.pdf Making Isabelle Content Accessible in Knowledge Representation Formats Michael Kohlhase, Florian Rabe, Makarius Wenzel 日付はハッキリしないが、2020以降なの…

WindowsのVoltaはかなり変な作りをしているらしい。C:/Program Files/Volta/ にある実行可能ファイルを実行すると、同名のcmdスクリプト/exeファイルを順番に再帰的にプロセス起動して、無限にプロセスを生成してしまう。C:/Program Files/Volta/ 内でプログ…

新しく導入する構文は： 変更可能代入文 副作用付きif文〈手続き的if文〉 キーワードと構文： let mut := 代入の右辺式は純 if-then-else if-then unless-do 翻訳： mutキーワードは、変数が変更可能であることを宣言する。let mut 変数 ← ... は、変更可能…

少しずつ説明。 構文範疇に、式と文〈ステートメント〉がある。 文には式文（式はそのまま文）と副作用let文がある。 do構文は式（do式）、純let式も式 let文といったときは副作用let文で、let式は純let式。 翻訳： do式の翻訳は、そのボディブロックを翻訳…

Voltaをバイナリでインストールした。 which node で C:\Program Files\Volta\node.exe それなら、C:\Program Files\nodejs\node.exe はいらないだろうとアンイストール。 node.exe を起動できなくなった。 どうやら、もともとあった node.js v16.14.0 をVol…