def uw_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32alg.bend:100

import Base

100def uw_zero(+n: Nat) -> {uw(n, Word.zero(n)) == 0n : Nat}:
101  match n:
102    case 0n:
103      {==}
104    case 1n+p:
105      %Equal.sym(Nat, uw(p, Word.zero(p)), 0n, uw_zero(p)) : {Nat.add(0n, Nat.double(_)) == 0n : Nat}
106      {==}