def carry

bend-kit-lemmas@0.1.1.0 · lemmas.bend:303

import Base

303# The carry out of Word.adc(n, a, b, False{}, c): the bit that a + b + c overflows into.
304def carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
305  match n:
306    case 0n:
307      c
308    case 1n+p:
309      match a b:
310        case WCon{x, at} WCon{y, bt}:
311          carry(p, at, bt, maj(x, y, c))