def u32.zero

bend-osdev-algo@0.1.0.0 · PROOF.bend:529

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

529def u32.zero(+x: U32, e: {A.bits32.word(x) == Word.zero(32n) : Word(32n)}) -> {x == 0 : U32}:
530  match x:
531    case U32{w}:
532      %e : {U32{w} == U32{_} : U32}
533      {==}