yoshihiro503 https://blog.hatena.ne.jp/yoshihiro503/ にわとり小屋でのプログラミング https://yosh.hateblo.jp/ Coq CPDT 変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。 Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. ここで binop型の値は二項演算子(binary operation)の種類(＋または×)を表すものとして以下で定義されるものとし、定数項は簡単のため自然数(nat)に限るとする。 Inductive binop : Set := Plus | Times. つまり、この定義のもとでは以下の… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fyosh.hateblo.jp%2Fentry%2F20100522%2Fp1" title="Coqで多変数多項式の簡約 - にわとり小屋でのプログラミング" 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 2010-05-22 00:00:00 rich https://yosh.hateblo.jp/entry/20100522/p1 1.0 100%