すべて | グループ指定なし | 定期チェック | NSFW | その他 | tom
おとなりアンテナ | おすすめページ
2024-11-10 (Sun)#1 Ltac2 でサブゴールを作るCoq においてゴール (サブゴールを含む) とは証明項の中の穴であり、証明を進めるというのはその穴を埋めていくことである。という素朴な理解でいままで済ましていたのだが、Ltac2 でサブゴールを作るのにはこの理解では足りなくて、いろいろ調べた。やりたいのは、Ltac2 で証明項を作る際に、その中にはサブゴールを入れて
