def finite

bendvy-ecs-core@0.1.0.4 · restore_raw_number.bend:15

import Base

15def finite(negative:Bool,high:U32,+low:U32,+exponent:U32) -> Checked:
16  match negative high low:
17    case False{} 0 0:Value{0}
18    case False{} 0 n:finite_checked(U32.is_ge(exponent,1074) && U32.is_le(exponent,1105) && U32.is_le(exponent,U32.add(1074,U32.sub(31,U32.from_nat(U32.log2(n))))),n,exponent)
19    case _ _ _:Invalid{}