MIPT-Coq-23-Lect-12

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: практическое доказывание теорем исчисления предикатов в конструктивном и классическом случаях; тактики enough, classical_left, classical_right; полиморфизм, неявные и “неявные максимально вставленные“ аргументы; примеры теорем о списках.