val eloc : Type0
let eloc = Ghost.erased B.loc
module WithLocal
module B = LowStar.Buffer
module HS = FStar.HyperStack
open FStar.HyperStack.ST
/
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
WithLocal.fst
Type0
FStar.Ghost.erased LowStar.Monotonic.Buffer.loc
let eloc =
  
Ghost.erased B.loc