def internal_inc_carry

bend-mathlib@0.8.1.0 · u32.bend:376

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

import Base

376def internal_inc_carry(n: Nat, w: Word(n)) -> Bool:
377  match n:
378    case 0n:
379      True{}
380    case 1n+p:
381      match w:
382        case WCon{False{}, t}:
383          False{}
384        case WCon{True{}, t}:
385          internal_inc_carry(p, t)

Uses (4)

Used by (3)