val t : a: Type0 -> Type0
let t (a:Type0) = ref (cell a)
module Selectors.PtrLList

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

module L = FStar.List.Tot

/// This module provides a variant of linked lists, where the list elements are themselves pointers.

/// Abstract type for a cell storing a value of type [a]
val cell (a:Type0) : Type0
/
Steel.Reference.fsti.checked Steel.Memory.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Selectors.PtrLList.fsti
a: Type0 -> Type0
Steel.Reference.ref Selectors.PtrLList.cell
let t (a: Type0) =
  
ref (cell a)