koba-e964 https://blog.hatena.ne.jp/koba-e964/ koba-e964の日記 https://koba-e964.hatenablog.com/ 最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。gist.github.com inaccessible termとは何か ".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分はパターンとしてではなく、項として一致するかどうかの検査が行われる。(つまり、パターン以外の項が書ける。) 項の部分は同じパターン内ですでに定義されている変数でなければならない。項の内部で新しい変数を導入することはできない。 使用例 埋め込んだコードのprim_evalの定義(ll. 36… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkoba-e964.hatenablog.com%2Fentry%2F2017%2F08%2F15%2F232816" title="Lean Proverのinaccessible termについて - koba-e964の日記" 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 2017-08-15 23:28:16 rich https://koba-e964.hatenablog.com/entry/2017/08/15/232816 1.0 100%