def fix_nz

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

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

1880def fix_nz(+a: U32, nz: {G.Gf8.is_zero(a) == False{} : Bool}) -> {fixz(G.Gf8.elt(a)) == G.Gf8.elt(a) : U32}:
1881  %Equal.sym(G.Gf8Bits, G.Gf8Bits.of(G.Gf8Bits.to(G.Gf8Bits.of(a))), G.Gf8Bits.of(a), ot(G.Gf8Bits.of(a))) : {Bool.pick(U32, G.Gf8Bits.is_zero(_), 1, G.Gf8.elt(a)) == G.Gf8.elt(a) : U32}
1882  %Equal.sym(Bool, G.Gf8.is_zero(a), False{}, nz) : {Bool.pick(U32, _, 1, G.Gf8.elt(a)) == G.Gf8.elt(a) : U32}
1883  {==}