qnikst
гинь-гинь idris plus_right_zero : (n, m : Nat) -> n + m = n -> m = 0
plus_right_zero _ Z Refl impossible
plus_right_zero (S ) Refl impossible

вот это мне сгенерировал идрис, и это прошло totality check, по его мнению n+m=n на натуральных числах невозможно
qnikst
Haskell idris Если вы встретите человека, который говорит что Haskell должен быть строгим по умолчанию — предложите ему пописать на Idris недельку
Zert
Erlang Haskell Agda Coq idris *хз
Нужен (не срочно, но час X всё ближе и ближе) экстрактор в ерланг из каких-нибудь зависимых типов. Ничего не нашёл. Есть чо?