def equal_decided

bendtorch-core@0.1.0.0 · src/shape/core.bend:548

import Base

548def equal_decided(+a: Nat, +b: Nat, decided: {True{} == Nat.is_eq(a, b) : Bool}) -> {a == b : Nat}:
549  match a b:
550    case 0n 0n:
551      {==}
552    case 0n 1n+q:
553      Empty.absurd({0n == 1n+q : Nat}, clash(decided))
554    case 1n+p 0n:
555      Empty.absurd({1n+p == 0n : Nat}, clash(decided))
556    case 1n+p 1n+q:
557      %equal_decided(p, q, decided) : {1n+p == 1n+_ : Nat}
558      {==}