val next (#a:Type0) (c:cell a) : t a
val next (#a:Type0) (c:cell a) : t a
let next #a (c:cell a) : t a = c.next
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
/
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
c: Selectors.PtrLList.cell a -> Selectors.PtrLList.t a
Selectors.PtrLList.cell Selectors.PtrLList.__proj__Mkcell__item__next Selectors.PtrLList.t
let next #a (c: cell a) : t a =
  
c.next