def add_sub

bend-ml-tensor-array@0.1.19.0 · main.bend:1551

import Base

1551# a <= r  ->  r == a + (r - a)
1552def add_sub(+a: Nat, +r: Nat, e: {True{} == leb(a, r) : Bool}) -> {r == Nat.add(a, Nat.sub(r, a)) : Nat}:
1553  match a r:
1554    case 0n 0n:
1555      {==}
1556    case 0n 1n+q:
1557      {==}
1558    case 1n+p 0n:
1559      %e : BD(_, Unit, {0n == Nat.add(1n+p, Nat.sub(0n, 1n+p)) : Nat})
1560      Unit{}
1561    case 1n+p 1n+q:
1562      %add_sub(p, q, e) : {1n+q == 1n+_ : Nat}
1563      {==}