MIPT-Coq-23-Lect-06

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: логическая интерпретация типов в \Lambda_\to; термы как доказательства; логическая семантика Брауера--Гейтинга--Колмогорова; первое знакомство Coq’ом и CoqIDE; тактики intro, exact, assumption и apply.