Интуиционистские связки (продолжение). Равенство

Пятница, 28 февраля 2020
Таймс, ауд. 410

Приложенные файлы

Описание

Добавим тривиально ложное и тривиально истинное утверждения и рассмотрим их соответствия в функциональном программировании. Посмотрим как закодировать (пропозициональное) равенство через индексированные индуктивные типы.