val vptr0 (#a: Type0) (r: ref a) (p: perm) : Tot vprop
let vptr0
  (#a: Type0)
  (r: ref a)
  (p: perm)
: Tot vprop
= vptr1 r p
val vptr0 (#a: Type0) (r: ref a) (p: perm) : Tot vprop
let vptr0 (#a: Type0) (r: ref a) (p: perm) : Tot vprop =
vptr1 r p
Steel.ArrayRef.fst.checked
Steel.Array.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fst
Steel.ArrayRef.ref Steel.FractionalPermission.perm Steel.ArrayRef.vptr1 Steel.Effect.Common.vprop
module Steel.ArrayRef

module A = Steel.Array

let null #a = A.null #a

let is_null r = A.is_null r

let vptr0_refine
  (#a: Type0)
  (r: ref a)
  (s: Seq.lseq a (A.length r))
: Tot prop
= Seq.length s == 1

let vptr0_rewrite
  (#a: Type)
  (r: ref a)
  (p: perm)
  (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
: Tot a
= Seq.index s 0

[@@__steel_reduce__; __reduce__]
let vptr1
  (#a: Type0)
  (r: ref a)
  (p: perm)
: Tot vprop
= A.varrayp r p `vrefine`
  vptr0_refine r `vrewrite`
  vptr0_rewrite r p

[@@__steel_reduce__]
let vptr0
  (#a: Type0)
  (r: ref a)
  (p: perm)
val vptr0 (#a: Type0) (r: ref a) (p: perm) : Tot vprop
r: Steel.ArrayRef.ref a -> p: Steel.FractionalPermission.perm -> Steel.Effect.Common.vprop