def allz

lawful-words@0.1.0.0 · proof_zb.bend:11

import Base

11# All bits clear.
12def allz(n: Nat, w: Word(n)) -> Bool:
13  match n:
14    case 0n:
15      True{}
16    case 1n+p:
17      match w:
18        case WCon{b, t}:
19          Bool.and(Bool.not(b), allz(p, t))