1

やや長い証明を書き終えましたが、試行するたびにQedエラーメッセージが表示されますError: This proof is focused, but cannot be unfocused this way。プルーフのフォーカスを外す他の方法はありますか? 私の証明は厳密ですが、私は単に認められたものを使用すべきですか? 参考までに、私はCoqIDE 8.6を使用しています

4

1 に答える 1