MIPT-Coq-24-Lect-06

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: Coq как язык программирования (обзор): термы, типы, сорта Prop и Set, редукции, рекурсивные определения, типы nat и list, полиморфизм; индуктивные типы на примере bool; индукция и рекурсия по типу bool; тактика split.