Я новичок в Coq. В настоящее время я полностью потерян в том, как должен выглядеть рабочий процесс.
Я доказываю теорему в Coqtop, используя тактику, а затем хочу сохранить код результата. Но когда я запускаю Print my_theorem., он показывает длинный и довольно низкоуровневый вывод вместо списка применяемых тактик. Как мне сохранить настойчивые результаты?
И есть ли полезные ресурсы, чтобы узнать больше о рабочем процессе Coq?