val data (c: cell) : a
val data (c: cell) : a
let data (c:cell) : a = LL.data c
module SelectorsLList2Example

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

module L = FStar.List.Tot
module LL = Selectors.LList2
module U32 = FStar.UInt32

inline_for_extraction noextract let a = U32.t
let cell = LL.cell a
/// The type of a list: A reference to a cell
let t = LL.t a
/
Steel.Reference.fsti.checked Steel.Memory.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked Selectors.LList2.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
SelectorsLList2Example.fst
c: SelectorsLList2Example.cell -> SelectorsLList2Example.a
SelectorsLList2Example.cell Selectors.LList2.data SelectorsLList2Example.a
let data (c: cell) : a =
  
LL.data c