def eq_rest

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

import Base

1593def eq_rest(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.sub(a, half(a)) == Nat.sub(b, half(b)) : Nat}:
1594  %e : {Nat.sub(a, half(a)) == Nat.sub(_, half(_)) : Nat}
1595  {==}