Очень заманчивая идея о том, как в Agda загнать под капот навязчивые subst и cong. Пример от автора.

Что-то попытки подключить к Агде унивалентность (отключив аксиому K) приводят к еженедельному обнаружению дырок в паттерн-матчинге. Вот опять сообщают. Следите за рассылкой, оставайтесь на острие.

К вопросу о заселении ⊥ при включенном type-in-type. Делается прямой реализацией парадокса Рассела

{-# OPTIONS --type-in-type --without-K ( Read more... )

Эти ваши интернеты бурлят:
ru-marazm.livejournal.com/3591670.html
lj.rossia.org/users/tiphareth/1685303.html
Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:
_*_ : ℕ → ℕ → ℕ zero * n = zero suc m * n = n + (m * n) Впрочем внучке стоило бы снять все вопросы, предоставив доказательство
*-commutative : ∀ m n → m * n ≡ n * m Взяв ( Read more... )

 
В современной теории типов выделяют два основных класса равенств: Definitional equality и Propositional equality. 
 ( Ого! Ну-ка, ну-ка... )

 Ян 

( Read more... )

Как лучше делать сопоставление с образцом в языке с зависимыми типами?
 

Coq's inductive types are implemented using separate "match" and "fix" constructions, which allow for deep matching, mutual matching, etc. Similarly, Agda allows function definition by pattern matching with a separate termination checker. However, this approach is only ( Read more... )

В Агде есть полезный зависимый тип данных - финитные натуральные. ( Кто они такие? )

Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. ( И мы знаем это число... )

Коллеги! Не будет ли слишком изощренным издевательством во вводной части обзора Агды, при самом начале обсуждения типа Vec привести такие примеры

[true,false,true] : Vec Bool 3
[2,12,85,0,6] : Vec ℕ 5
Поясню - я не хочу в этом месте вдаваться в детали описания конструкторов, а скрытый здесь грандиозный обман я честным образом раскрою позже.