Logic_J.vまで一応読了。分からん問題は答え見てもさっぱり分からん。 殊にappears_inがらみがまるで歯が立たなかった。途中 一つQed.を書き忘れて、 Error: There are pending proofsとかエラーが出てcoqcが失敗して難儀した。括弧の対応が取れてないような…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。