val array_nth (#ty: Type) (a: array_t ty) (i: nat) : option ty
val array_nth (#ty: Type) (a: array_t ty) (i: nat) : option ty
let array_nth (#ty: Type) (a: array_t ty) (i: nat) : option ty =
  if i >= array_len a then
    None
  else
    Some (array_index a i)
module Util.ImmutableArray

open FStar.ImmutableArray
open Spec.List
open Spec.Ubool
open Util.List
open Util.Nth
open Util.Range

let array_t = FStar.ImmutableArray.t
let array_len = FStar.ImmutableArray.length
let array_index = FStar.ImmutableArray.index
let list_to_array = FStar.ImmutableArray.of_list
let array_to_list = FStar.ImmutableArray.to_list
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.ImmutableArray.fsti.checked
Util.ImmutableArray.fsti
a: Util.ImmutableArray.array_t ty -> i: Prims.nat -> FStar.Pervasives.Native.option ty
Util.ImmutableArray.array_t Prims.nat Prims.op_GreaterThanOrEqual Util.ImmutableArray.array_len FStar.Pervasives.Native.None Prims.bool FStar.Pervasives.Native.Some Util.ImmutableArray.array_index FStar.Pervasives.Native.option
let array_nth (#ty: Type) (a: array_t ty) (i: nat) : option ty =
  
if i >= array_len a then None else Some (array_index a i)