law Word.sub_add

bend-lawful-stdlib@0.1.0.0 · src/u32.bend:213

import Base

213# (a + b + c) - b, with carry not(c), is a. Each case passes the carry
214# out of its bit.
215law Word.sub_add:
216  for +n: Nat
217  for a: Word(n)
218  for +b: Word(n)
219  for c: Bool
220  {a == Word.adc(n, Word.adc(n, a, b, False{}, c), b, True{}, Bool.not(c)) : Word(n)}