val triv : LowStar.Monotonic.Buffer.srel LowParse.Bytes.byte
let triv = B.trivial_preorder LowParse.Bytes.byte
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

inline_for_extraction
/
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked LowParse.Bytes.fsti.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.fsti
LowStar.Monotonic.Buffer.srel LowParse.Bytes.byte
LowStar.Buffer.trivial_preorder LowParse.Bytes.byte
let triv =
  
B.trivial_preorder LowParse.Bytes.byte