def internal_carry

bend-mathlib@0.8.1.0 · u32.bend:182

import bend-mathlib@0.8.1.0/u32.bend as U32
import Base

182def internal_carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
183  match n:
184    case 0n:
185      c
186    case 1n+p:
187      match a b:
188        case WCon{False{}, at} WCon{+bb, bt}:
189          internal_carry(p, at, bt, Bool.and(bb, c))
190        case WCon{True{}, at} WCon{+bb, bt}:
191          internal_carry(p, at, bt, Bool.or(bb, c))

Uses (6)

Used by (5)