val of_double32 (q:double32) : poly
let of_double32 d = of_double32_def d
val of_double32 (q:double32) : poly
let of_double32 d =
of_double32_def d
Vale.Math.Poly2.Bits_s.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Bits_s.fst
Vale.Def.Types_s.double32 Vale.Math.Poly2.Bits_s.of_double32_def Vale.Math.Poly2_s.poly
module Vale.Math.Poly2.Bits_s
open FStar.Mul
val of_double32 (q:double32) : poly
q: Vale.Def.Types_s.double32 -> Vale.Math.Poly2_s.poly