val hide_ref (#a: Type u#1) (r: Steel.ST.HigherReference.ref a) : Pure (ref a)
  (requires True)
  (ensures (fun r' -> reveal_ref r' == r))
let hide_ref r = Hide r
val hide_ref (#a: Type u#1) (r: Steel.ST.HigherReference.ref a) : Pure (ref a)
  (requires True)
  (ensures (fun r' -> reveal_ref r' == r))
let hide_ref r =
Hide r
Steel.ST.GhostHigherReference.fst.checked
Steel.ST.HigherReference.fst.checked Steel.ST.Coercions.fsti.checked Steel.HigherReference.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GhostHigherReference.fst
Steel.ST.HigherReference.ref Steel.ST.GhostHigherReference.Hide Steel.ST.GhostHigherReference.ref
module Steel.ST.GhostHigherReference

// needed because I need to know that `Steel.ST.HigherReference.ref a`
// can be turned into `Steel.HigherReference.ref a`
friend Steel.ST.HigherReference

module RST = Steel.ST.HigherReference
module R = Steel.HigherReference

module STC = Steel.ST.Coercions

// FIXME: WHY WHY WHY in `Ghost.reveal (ref a)` is `a` not strictly positive?

[@@erasable]
noeq
type ref' ([@@@strictly_positive] a : Type u#1) : Type0
= | Hide: (reveal: R.ref a) -> ref' a

let ref a = ref' a

let pts_to r p v = RST.pts_to r.reveal p v

let reveal_ref r = r.reveal
val hide_ref (#a: Type u#1) (r: Steel.ST.HigherReference.ref a) : Pure (ref a)
  (requires True)
  (ensures (fun r' -> reveal_ref r' == r))
r: Steel.ST.HigherReference.ref a -> Prims.Pure (Steel.ST.GhostHigherReference.ref a)