val to_quad32 (a:poly) : quad32
let to_quad32 a = to_quad32_def a
val to_quad32 (a:poly) : quad32
let to_quad32 a =
to_quad32_def a
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.Math.Poly2_s.poly Vale.Math.Poly2.Bits_s.to_quad32_def Vale.Def.Types_s.quad32
module Vale.Math.Poly2.Bits_s
open FStar.Mul

let to_double32 a = to_double32_def a
val to_quad32 (a:poly) : quad32
a: Vale.Math.Poly2_s.poly -> Vale.Def.Types_s.quad32