• гинь-гинь 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 на натуральных числах невозможно
    ♡ recommended by @ndtimofeev, @blaze

Replies (0)