def natural_equal

bendtorch-core@0.1.0.0 · src/tensor/lifecycle.bend:138

import Base

138def natural_equal(+a: Nat, +b: Nat, equal: {True{} == Nat.is_eq(a, b) : Bool}) -> {a == b : Nat}:
139  match a b:
140    case 0n 0n:
141      {==}
142    case 0n 1n+q:
143      Empty.absurd({0n == 1n+q : Nat}, false_true(equal))
144    case 1n+p 0n:
145      Empty.absurd({1n+p == 0n : Nat}, false_true(equal))
146    case 1n+p 1n+q:
147      Equal.cong(Nat, Nat, x => 1n+x, p, q, natural_equal(p, q, equal))