def ud.r
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOFimport Base
1483def ud.r(m: Nat, qr: Word(m) & U32) -> Nat:
1484 (q, r) = qr
1485 U32.to_nat(r)
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOFimport Base
1483def ud.r(m: Nat, qr: Word(m) & U32) -> Nat:
1484 (q, r) = qr
1485 U32.to_nat(r)