Формализуем изоморфизм Карри-Говарда на Agda
Jul 21, 2017 · 1 min read

Программируем с зависимыми типами на русском. На самом деле там совсем небольшой фрагмент реализован, чисто посмотреть. Сначала сделал нормально, потом захотелость *полной мощи юникода*. Определения и переводы вышли странные (Связка? лол), верить им ни в коем случае нельзя.
Вот вам пример:
сделать_Δ_из : Список Φ → Список Связка
сделать_Δ_из формулы =
отобразить (λ φ → ("x_" конкатенировать φ встроку) типа Φ→Π φ)
на формулыФулл версия (для нашего и вашего увеселения):
