val hide:
    #a:Type
  -> s:S.seq a{S.length s < pow2 32}
  -> GTot (raw a (U32.uint_to_t (S.length s)))
let hide #a s = s
val hide:
    #a:Type
  -> s:S.seq a{S.length s < pow2 32}
  -> GTot (raw a (U32.uint_to_t (S.length s)))
let hide #a s =
s
FStar.Vector.Base.fst.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
FStar.Vector.Base.fst
FStar.Seq.Base.seq Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Prims.pow2 FStar.Vector.Base.raw FStar.UInt32.uint_to_t
(*
      Copyright 2008-2017 Microsoft Research

      Licensed under the Apache License, Version 2.0 (the "License");
      you may not use this file except in compliance with the License.
      You may obtain a copy of the License at

          http://www.apache.org/licenses/LICENSE-2.0

      Unless required by applicable law or agreed to in writing, software
      distributed under the License is distributed on an "AS IS" BASIS,
      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
      See the License for the specific language governing permissions and
      limitations under the License.
*)
module FStar.Vector.Base
module U32 = FStar.UInt32
module S = FStar.Seq

/// The raw vector type: the main type provided by this module
let raw a l = s:S.seq a{S.length s = U32.v l}

/// Abstractly, a `raw a l` is just a sequence whose length is `U32.v l`.
/// `reveal` and `hide` build an isomorphism establishing this
val hide:
    #a:Type
  -> s:S.seq a{S.length s < pow2 32}
  -> GTot (raw a (U32.uint_to_t (S.length s)))
s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s < Prims.pow2 32}
  -> Prims.GTot (FStar.Vector.Base.raw a (FStar.UInt32.uint_to_t (FStar.Seq.Base.length s)))