MIPT-Coq-25-Lect-07

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: импликативный фрагмент интуиционистской логики высказываний в Coq (продолжение); функциональное программирование в Coq.