def eq_true

bendtorch-core@0.1.0.0 · src/storage/arith.bend:61

import Base

61def eq_true(+a: Nat, +b: Nat, decided: {Nat.is_eq(a, b) == True{} : Bool}) -> {a == b : Nat}:
62  match a b:
63    case 0n 0n:
64      {==}
65    case 0n 1n+q:
66      Empty.absurd({0n == 1n+q : Nat}, clash(decided))
67    case 1n+p 0n:
68      Empty.absurd({1n+p == 0n : Nat}, clash(decided))
69    case 1n+p 1n+q:
70      %eq_true(p, q, decided) : {1n+p == 1n+_ : Nat}
71      {==}