def h.isz

bend-kit-collections@0.1.4.1 · PROOF.bend:1820

import Base

1820# A mask with at most one set bit routes every hash to one of two sides.
1821def h.isz(n: Nat, w: Word(n)) -> Bool:
1822  match n:
1823    case 0n:
1824      True{}
1825    case 1n+p:
1826      match w:
1827        case WCon{b, t}:
1828          Bool.not(b) && h.isz(p, t)