MIPT-Coq-CyPr-23-Lect-07

Основы инженерии доказательств (Coq) в МФТИ. Темы: дальнейшие примеры тактикалов; Coq как язык функционального программирования (первые примеры) — индуктивные типы nat, bool, list A, сорта Set и Prop, сравнение с образцом (pattern matching), рекурсия, списки.