MIPT-Coq-CyPr-23-Lect-12

Основы инженерии доказательств (Coq) в МФТИ. Темы: представление равенства с помощью индуктивных типов; доказывание неравенств между конструкторами индуктивных типов; вычисления при проверке типа — некоторые трюки; практическое доказывание теорем в конструктивной и классической логиках высказываний и предикатов.