val loc_perm (#t: _) (#b: B.buffer t) (p: perm b) : GTot B.loc
let loc_perm p = B.loc_buffer p
val loc_perm (#t: _) (#b: B.buffer t) (p: perm b) : GTot B.loc
let loc_perm p =
B.loc_buffer p
EverParse3d.Readable.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
EverParse3d.Readable.fst
LowStar.Buffer.buffer EverParse3d.Readable.perm LowStar.Monotonic.Buffer.loc_buffer FStar.Ghost.erased FStar.Seq.Base.seq Prims.bool LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.loc
module EverParse3d.Readable

let perm0 t = B.pointer (Ghost.erased (Seq.seq bool))

let perm_prop p b = B.loc_disjoint (B.loc_buffer b) (B.loc_buffer p) /\ True
val loc_perm (#t: _) (#b: B.buffer t) (p: perm b) : GTot B.loc
p: EverParse3d.Readable.perm b -> Prims.GTot LowStar.Monotonic.Buffer.loc