val is_null (#a:Type0) (r:ref a) : (b:bool{b <==> r == null})
let is_null r = A.is_null r
val is_null (#a:Type0) (r:ref a) : (b:bool{b <==> r == null})
let is_null r =
A.is_null r
Steel.ArrayRef.fst.checked
Steel.Array.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fst
Steel.ArrayRef.ref Steel.ST.Array.is_null Prims.bool Prims.l_iff Prims.b2t Prims.eq2 Steel.ArrayRef.null
module Steel.ArrayRef

module A = Steel.Array

let null #a = A.null #a
val is_null (#a:Type0) (r:ref a) : (b:bool{b <==> r == null})
r: Steel.ArrayRef.ref a -> b: Prims.bool{b <==> r == Steel.ArrayRef.null}