val coerce (#a: Type) (#l: len_t) (v: raw a l) (m: len_t{l == m}) : Tot (raw a m)
let coerce
    (#a:Type)
    (#l:len_t)
    (v:raw a l)
    (m:len_t{l == m})
  : Tot (raw a m)
  = v
val coerce (#a: Type) (#l: len_t) (v: raw a l) (m: len_t{l == m}) : Tot (raw a m)
let coerce (#a: Type) (#l: len_t) (v: raw a l) (m: len_t{l == m}) : Tot (raw a m) =
v
FStar.Vector.Properties.fst.checked
prims.fst.checked FStar.Vector.Base.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
FStar.Vector.Properties.fst
FStar.Vector.Base.len_t FStar.Vector.Base.raw Prims.eq2
(*
      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.Properties
open FStar.Vector.Base
module S = FStar.Seq
module U32 = FStar.UInt32

/// This coercion seems to be necessary in some places
///
/// For example,  when trying to treat a    `raw a (l1 +^ l2)`
///                                    as a `raw a (m1 +^ m2)`
/// F* type inference tries matches on the head symbol of the index
/// and tries to prove `l1 = m1 /\ l2 = m2`
/// which is often too strong.
/// This coercion is a workaround for in such cases
unfold
let coerce
    (#a:Type)
    (#l:len_t)
    (v:raw a l)
    (m:len_t{l == m})
val coerce (#a: Type) (#l: len_t) (v: raw a l) (m: len_t{l == m}) : Tot (raw a m)
v: FStar.Vector.Base.raw a l -> m: FStar.Vector.Base.len_t{l == m} -> FStar.Vector.Base.raw a m