def incc

lawful-words@0.1.0.0 · proof_word.bend:312

import Base

312# The carry out of Word.inc: set when every bit is set.
313def incc(n: Nat, w: Word(n)) -> Bool:
314  match n:
315    case 0n:
316      True{}
317    case 1n+p:
318      match w:
319        case WCon{False{}, t}:
320          False{}
321        case WCon{True{}, t}:
322          incc(p, t)