← All posts tagged idris

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 недельку