def cout

lawful-words@0.1.0.0 · proof_word.bend:353

import Base

353# The carry out of Word.adc without inversion (f = False).
354def cout(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
355  match n:
356    case 0n:
357      c
358    case 1n+p:
359      match a b:
360        case WCon{False{}, at} WCon{bb, bt}:
361          cout(p, at, bt, Bool.and(bb, c))
362        case WCon{True{}, at} WCon{bb, bt}:
363          cout(p, at, bt, Bool.or(bb, c))