val len_all (x: t) : GTot LPE.pos_t
let len_all
  (x: t)
: GTot LPE.pos_t
= if x.Aux.has_length
  then x.Aux.length
  else Aux.len_all x.Aux.base
val len_all (x: t) : GTot LPE.pos_t
let len_all (x: t) : GTot LPE.pos_t =
if x.Aux.has_length then x.Aux.length else Aux.len_all x.Aux.base
EverParse3d.InputStream.Extern.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.InputStream.Extern.Type.fst.checked EverParse3d.ErrorCode.fst.checked
EverParse3d.InputStream.Extern.fst
EverParse3d.InputStream.Extern.t EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__has_length EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__length Prims.bool EverParse3d.InputStream.Extern.Base.len_all EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__base EverParse3d.ErrorCode.pos_t
module EverParse3d.InputStream.Extern

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module U64 = FStar.UInt64
module LPE = EverParse3d.ErrorCode

module Aux = EverParse3d.InputStream.Extern.Type

inline_for_extraction
noextract
let t = Aux.input_buffer

let len_all
  (x: t)
val len_all (x: t) : GTot LPE.pos_t
x: EverParse3d.InputStream.Extern.t -> Prims.GTot EverParse3d.ErrorCode.pos_t