val buffer_or_null_loc_addr (#a: Type0) (b: buffer a) : GTot B.loc
val buffer_or_null_loc_addr (#a: Type0) (b: buffer a) : GTot B.loc
let buffer_or_null_loc_addr (#a:Type0) (b:buffer a) : GTot B.loc =
  if B.g_is_null b then B.loc_buffer b // For some reason, we need to return loc_buffer b (and not loc_none)
  else B.loc_addr_of_buffer b
module Impl.Noise.TypeOrUnit

open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Sequence
open Lib.Buffer
open LowStar.BufferOps

module B = LowStar.Buffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
open Impl.Noise.Types
open Spec.Noise

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
/
Spec.Noise.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.TypeOrUnit.fsti
b: Lib.Buffer.buffer a -> Prims.GTot LowStar.Monotonic.Buffer.loc
Lib.Buffer.buffer LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.loc_buffer Prims.bool LowStar.Monotonic.Buffer.loc_addr_of_buffer LowStar.Monotonic.Buffer.loc
let buffer_or_null_loc_addr (#a: Type0) (b: buffer a) : GTot B.loc =
  
if B.g_is_null b then B.loc_buffer b else B.loc_addr_of_buffer b