def un.co

bend-osdev-u32@0.1.0.0 · PROOF.bend:510

import Base

510def un.co(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
511  match n:
512    case 0n:
513      c
514    case 1n+p:
515      match a b:
516        case WCon{x, at} WCon{y, bt}:
517          un.co(p, at, bt, un.maj(x, y, c))