MIPT-Coq-24-Lect-07

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: примеры индуктивных типов и теорем для них (продолжение): bool, nat, двоичные деревья; тактики induction, destruct, simpl, rewrite, clear; команда Search; прямое произведение типов: квантор всеобщности и импликация.

Видео MIPT-Coq-24-Lect-07 автора evgeny.dashkov