def internal_u32_cmp_refl

bend-mathlib@0.8.1.0 · string.bend:139

import Base

139def internal_u32_cmp_refl(x: U32) -> {EQ{} == U32.cmp(x, x) : Cmp}:
140  match x:
141    case U32{w}:
142      %internal_word_cmp_refl(32n, w) : {EQ{} == _ : Cmp}
143      {==}