def is_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/src/wide.bend:30

import Base

30def is_zero(n: Nat, w: Word(n)) -> Bool:
31  match n:
32    case 0n:
33      True{}
34    case 1n+p:
35      match w:
36        case WCon{b, tail}:
37          Bool.not(b) && is_zero(p, tail)