一日寝てた。 昨日のCoq 別に間違っておらんかった。間違ってたのは、omegaの使い方のようだ。 詰るところ使い方がわからん。 数値定数、加算(+とS)、減算(-とpred)、 定数の積算(これがプレスバーガー算術である条件です)、 等式(=と<>)および不等式( 論理…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。