val mk_cell (n: t) (d: a) : Pure cell (requires True) (ensures fun c -> next c == n /\ data c == d)
val mk_cell (n: t) (d: a) : Pure cell (requires True) (ensures fun c -> next c == n /\ data c == d)
let mk_cell (n: t) (d:a)
  : Pure cell
    (requires True)
    (ensures fun c ->
      next c == n /\
      data c == d)
= LL.mk_cell n d
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

let next (c:cell) : t = LL.next c
/
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
n: SelectorsLList2Example.t -> d: SelectorsLList2Example.a -> Prims.Pure SelectorsLList2Example.cell
SelectorsLList2Example.t SelectorsLList2Example.a Selectors.LList2.mk_cell SelectorsLList2Example.cell Prims.l_True Prims.l_and Prims.eq2 SelectorsLList2Example.next SelectorsLList2Example.data
let mk_cell (n: t) (d: a) : Pure cell (requires True) (ensures fun c -> next c == n /\ data c == d) =
  
LL.mk_cell n d