val mk_cell (#a:Type0) (n: t a) (d:ref a)
  : Pure (cell a)
    (requires True)
    (ensures fun c ->
      next c == n /\
      data c == d)
val mk_cell (#a:Type0) (n: t a) (d:ref a)
  : Pure (cell a)
    (requires True)
    (ensures fun c ->
      next c == n /\
      data c == d)
let mk_cell #a (n: t a) (d:ref a) = {
  next = n;
  data = d
}
module Selectors.PtrLList

open FStar.Ghost
open Steel.FractionalPermission
module Mem = Steel.Memory

open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference

#push-options "--__no_positivity"
noeq
type cell (a:Type0) = {
  next : ref (cell a);
  data : ref a;
}
#pop-options

let next #a (c:cell a) : t a = c.next
/
Steel.Reference.fsti.checked Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Selectors.PtrLList.fst
n: Selectors.PtrLList.t a -> d: Steel.Reference.ref a -> Prims.Pure (Selectors.PtrLList.cell a)
Selectors.PtrLList.t Steel.Reference.ref Selectors.PtrLList.Mkcell Selectors.PtrLList.cell
let mk_cell #a (n: t a) (d: ref a) =
  
{ next = n; data = d }