val length (#b: _) (vb:buffer b)
  : GTot nat
let length #b vb = B.length (as_buffer vb) / View?.n (get_view vb)
val length (#b: _) (vb:buffer b)
  : GTot nat
let length #b vb =
B.length (as_buffer vb) / View?.n (get_view vb)
LowStar.BufferView.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
LowStar.BufferView.fst
LowStar.BufferView.buffer Prims.op_Division LowStar.Monotonic.Buffer.length FStar.Pervasives.__proj__Mkdtuple4__item___1 LowStar.Monotonic.Buffer.srel LowStar.BufferView.buffer_view FStar.Pervasives.__proj__Mkdtuple4__item___2 FStar.Pervasives.__proj__Mkdtuple4__item___3 LowStar.BufferView.as_buffer LowStar.BufferView.__proj__View__item__n LowStar.BufferView.get_view Prims.nat
(*
   Copyright 2008-2018 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 LowStar.BufferView

noeq
type buffer_view (a:Type0) (rrel rel:B.srel a) (b:Type u#b) : Type u#b =
  | BufferView: buf:B.mbuffer a rrel rel
              -> v:view a b{B.length buf % View?.n v == 0}
              -> buffer_view a rrel rel b

let mk_buffer_view #src #rrel #rel #dest b v  = (| src, rrel, rel, BufferView b v |)

let as_buffer #b v = BufferView?.buf (Mkdtuple4?._4 v)

let as_buffer_mk_buffer_view #_ #_ #_ #_ _ _ = ()

let get_view #b v = BufferView?.v (Mkdtuple4?._4 v)

let get_view_mk_buffer_view #_ #_ #_ #_ _ _ = ()
val length (#b: _) (vb:buffer b)
  : GTot nat
vb: LowStar.BufferView.buffer b -> Prims.GTot Prims.nat