def u.refl

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:286

import Base

286def u.refl(a: U32) -> {U32.cmp(a, a) == EQ{} : Cmp}:
287  match a:
288    case U32{+w}:
289      wd.refl(32n, w)