val is_null (ptr: t) : (b: bool{b <==> ptr == null_llist ()})
val is_null (ptr: t) : (b: bool{b <==> ptr == null_llist ()})
let is_null (ptr:t) : (b:bool{b <==> ptr == null_llist ()})
= LL.is_null ptr
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
let data (c:cell) : a = LL.data c
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

/// The null list pointer
let null_llist () : t = LL.null_llist
/
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
ptr: SelectorsLList2Example.t -> b: Prims.bool{b <==> ptr == SelectorsLList2Example.null_llist ()}
SelectorsLList2Example.t Selectors.LList2.is_null SelectorsLList2Example.a Prims.bool Prims.l_iff Prims.b2t Prims.eq2 SelectorsLList2Example.null_llist
let is_null (ptr: t) : (b: bool{b <==> ptr == null_llist ()}) =
  
LL.is_null ptr