val ref (a: Type0) : Type0
let ref (a : Type0) : Type0 = (r: A.array a { A.length r == 1 \/ r == A.null })
val ref (a: Type0) : Type0
let ref (a: Type0) : Type0 =
(r: A.array a {A.length r == 1 \/ r == A.null})
Steel.ArrayRef.fsti.checked
Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Common.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked Steel.Array.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fsti
Steel.ST.Array.array Prims.l_or Prims.eq2 Prims.int Steel.ST.Array.length Steel.ST.Array.null
module Steel.ArrayRef

open Steel.FractionalPermission
open Steel.Memory
open Steel.Effect.Common
open Steel.Effect
open Steel.Effect.Atomic

module A = Steel.Array

(** This module provides the same interface as Steel.Reference, however, it builds on top
    of Steel.Array to enable the interoperation between arrays and references.
    Similarly to C, a reference is defined as an array of length 1 *)

/// An abstract datatype for references
val ref (a: Type0) : Type0
a: Type0 -> Type0