val to_uint (n: pos) (a: poly) : uint_t n
let to_uint (n:pos) (a:poly) : uint_t n =
  from_vec #n (to_seq (reverse a (n - 1)) n)
val to_uint (n: pos) (a: poly) : uint_t n
let to_uint (n: pos) (a: poly) : uint_t n =
from_vec #n (to_seq (reverse a (n - 1)) n)
Vale.Math.Poly2.Bits_s.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Bits_s.fsti
Prims.pos Vale.Math.Poly2_s.poly FStar.UInt.from_vec Vale.Math.Poly2_s.to_seq Vale.Math.Poly2_s.reverse Prims.op_Subtraction FStar.UInt.uint_t
module Vale.Math.Poly2.Bits_s
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Math.Poly2_s
open FStar.Seq
open FStar.UInt

// Bit-level representations of poly, expressed in terms of FStar.UInt.uint_t.
// Least-significant bit represents x^0, next bit represents x^1, etc.
// (Note that FStar.UInt uses 0 for most-significant bit,
// so definitions below use "reverse" to compensate.)
val to_uint (n: pos) (a: poly) : uint_t n
n: Prims.pos -> a: Vale.Math.Poly2_s.poly -> FStar.UInt.uint_t n