Равенство (продолжение). Кванторы всеобщности и существования
Пятница, 06 марта 2020
Таймс, ауд. 410
Продолжим рассмотрение зависимого сопоставления с образцом: инъективность и непересекаемость конструкторов индуктивных типов, паттерн конвой
.
Моделирование кванторов всеобщности и существования в Coq.