おとなりアンテナ | おすすめページ
2024-04-09 (Tue)#1 Coq の P -> False を ~P に変える先に結論を書いておく: change (~ P) もしくは change (?p -> False) with (~ p) を使えばよいCoq で、~P というのは、not P の notation である。not は以下のように定義される。Definition not := fun A : Pro
