kikx https://blog.hatena.ne.jp/kikx/ 菊やんの雑記帳 https://kikx.hatenadiary.org/ Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。 Section Hoge. Variable x : nat. Definition foo := x + 1. Definition bar := foo + 2. (* Section の中では x はグローバル変数みたいに使える *) End Hoge. (* Section を閉じると、foo と bar は x を引数にとるようになる *) Definition baz := bar 42.この機能とポインタを一緒に使うと変更できるグローバル変数みたいに使えます。 Section Foo. (* 最後にスロット… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkikx.hatenadiary.org%2Fentry%2F20110621%2F1308621323" title=" セクション - 菊やんの雑記帳" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2011-06-21 10:55:23 rich https://kikx.hatenadiary.org/entry/20110621/1308621323 1.0 100%