def double

stelliferous@0.0.2.0 · proofs/u32_shift.bend:103

import Base

103def double(+x: U32,h: {U32.is_lt(x,2147483648) == True{} : Bool}) -> {U32.to_nat(U32.shl(x)) == Nat.double(U32.to_nat(x)) : Nat}:
104  match x:
105    case U32{w}:
106      double_word(w)(h)