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