let lbuffer (l:nat) = b:Buffer.buffer UInt8.t {Buffer.length b == l}
let lbuffer (l: nat) =
b: Buffer.buffer UInt8.t {Buffer.length b == l}
Test.BufferBytes.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.IO.fst.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked FStar.Buffer.fst.checked C.fst.checked BufferBytes.fsti.checked
Test.BufferBytes.fst
Prims.nat FStar.Buffer.buffer FStar.UInt8.t Prims.eq2 FStar.Buffer.length
module Test.BufferBytes

open FStar.Bytes
open FStar.Error
open FStar.Printf
open FStar.HyperStack
open FStar.HyperStack.IO
open FStar.HyperStack.ST

module BB = BufferBytes
val lbuffer : l: Prims.nat -> Type0
l: Prims.nat -> Type0