MIPT-Coq-22-Lect-04

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: свойства лямбда-исчисления с простыми типами; программирование в нем; интерпретация BHK, система натурального вывода и доказательства в Coq для импликативного фрагмента интуиционистского исчисления высказываний; тактики exact, intro и apply. ======== Если видео показалось вам полезным, вы можете поддержать автора: === If you have found this video helpful, you might want to support the author: === BTC: bc1q3p5x57cppjs0rfgj5f406yrljxylg96seed0t4