def fixm_nz

bend-osdev-gf@0.1.1.0 · PROOF.bend:7560

import Base

7560def fixm_nz(+x: U32, nz: {U32.is_eq(x, 0) == False{} : Bool}) -> {fixm(x) == x : U32}:
7561  %Equal.sym(Bool, U32.is_eq(x, 0), False{}, nz) : {Bool.pick(U32, _, 1, x) == x : U32}
7562  {==}