val slice_of (#len: U32.t) (x: input_buffer_t len) : GTot (sl: slice triv triv { sl.LPL.len == len })
let slice_of #len x =
  { LPL.base = x; LPL.len = len }
val slice_of (#len: U32.t) (x: input_buffer_t len) : GTot (sl: slice triv triv { sl.LPL.len == len })
let slice_of #len x =
{ LPL.base = x; LPL.len = len }
EverParse3d.InputBuffer.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.Readable.fsti.checked
EverParse3d.InputBuffer.fst
FStar.UInt32.t EverParse3d.InputBuffer.input_buffer_t LowParse.Slice.Mkslice EverParse3d.InputBuffer.triv LowParse.Slice.slice Prims.eq2 LowParse.Slice.__proj__Mkslice__item__len
module EverParse3d.InputBuffer

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module LPL = LowParse.Low.Base
module R = EverParse3d.Readable
module G = FStar.Ghost

open LowParse.Low.Base

let input_buffer_t len =
  (base: B.buffer LPL.byte { U32.v len <= B.length base })
val slice_of (#len: U32.t) (x: input_buffer_t len) : GTot (sl: slice triv triv { sl.LPL.len == len })
x: EverParse3d.InputBuffer.input_buffer_t len
  -> Prims.GTot
    (sl:
      LowParse.Slice.slice EverParse3d.InputBuffer.triv EverParse3d.InputBuffer.triv
        {Mkslice?.len sl == len})