val array_matches_list (#ty: Type) (a: array_t ty) (l: list ty) : GTot bool
val array_matches_list (#ty: Type) (a: array_t ty) (l: list ty) : GTot bool
let array_matches_list (#ty: Type) (a: array_t ty) (l: list ty) : GTot bool =
  array_offset_matches_list a (array_len a) 0 l
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

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)

let rec array_offset_matches_list
  (#ty: Type)
  (a: array_t ty)
  (len: nat{len = array_len a})
  (offset: nat)
  (l: list ty)
  : GTot bool (decreases l) =
  match l with
  | [] -> len = offset
  | hd :: tl -> len > offset && eqb hd (array_index a offset) && array_offset_matches_list a len (offset + 1) tl
/
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 -> l: Prims.list ty -> Prims.GTot Prims.bool
Util.ImmutableArray.array_t Prims.list Util.ImmutableArray.array_offset_matches_list Util.ImmutableArray.array_len Prims.bool
let array_matches_list (#ty: Type) (a: array_t ty) (l: list ty) : GTot bool =
  
array_offset_matches_list a (array_len a) 0 l