val seq_list_match
      (#t #t': Type)
      (c: Seq.seq t)
      (v: list t')
      (item_match: (t -> v': t'{v' << v} -> vprop))
    : Tot vprop (decreases v)
let rec seq_list_match
  (#t #t': Type)
  (c: Seq.seq t)
  (v: list t')
  (item_match: (t -> (v': t' { v' << v }) -> vprop))
: Tot vprop
  (decreases v)
= if Nil? v
  then seq_list_match_nil0 c
  else seq_list_match_cons0 c v item_match seq_list_match
val seq_list_match
      (#t #t': Type)
      (c: Seq.seq t)
      (v: list t')
      (item_match: (t -> v': t'{v' << v} -> vprop))
    : Tot vprop (decreases v)
let rec seq_list_match
      (#t #t': Type)
      (c: Seq.seq t)
      (v: list t')
      (item_match: (t -> v': t'{v' << v} -> vprop))
    : Tot vprop (decreases v) =
if Nil? v then seq_list_match_nil0 c else seq_list_match_cons0 c v item_match seq_list_match
Steel.ST.SeqMatch.fst.checked
Steel.ST.OnRange.fsti.checked Steel.ST.GenElim.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Steel.ST.SeqMatch.fst
FStar.Seq.Base.seq Prims.list Prims.precedes Steel.Effect.Common.vprop Prims.uu___is_Nil Steel.ST.SeqMatch.seq_list_match_nil0 Prims.bool Steel.ST.SeqMatch.seq_list_match_cons0 Steel.ST.SeqMatch.seq_list_match
module Steel.ST.SeqMatch
include Steel.ST.OnRange
open Steel.ST.GenElim

module Seq = FStar.Seq
module SZ = FStar.SizeT

(* `seq_list_match` describes how to match a sequence of low-level
values (the low-level contents of an array) with a list of high-level
values. `seq_list_match` is carefully designed to be usable within
(mutually) recursive definitions of matching functions on the type of
high-level values.  *)

[@@__reduce__]
let seq_list_match_nil0
  (#t: Type)
  (c: Seq.seq t)
: Tot vprop
= pure (c `Seq.equal` Seq.empty)

[@@__reduce__]
let seq_list_match_cons0
  (#t #t': Type)
  (c: Seq.seq t)
  (l: list t' { Cons? l })
  (item_match: (t -> (v': t' { v' << l }) -> vprop))
  (seq_list_match: (Seq.seq t -> (v': list t') -> (raw_data_item_match: (t -> (v'': t' { v'' << v' }) -> vprop) { v' << l }) ->
vprop))
: Tot vprop
= exists_ (fun (c1: t) -> exists_ (fun (c2: Seq.seq t) ->
    item_match c1 (List.Tot.hd l) `star`
    seq_list_match c2 (List.Tot.tl l) item_match `star`
    pure (c `Seq.equal` Seq.cons c1 c2)
  ))

let rec seq_list_match
  (#t #t': Type)
  (c: Seq.seq t)
  (v: list t')
  (item_match: (t -> (v': t' { v' << v }) -> vprop))
: Tot vprop
val seq_list_match
      (#t #t': Type)
      (c: Seq.seq t)
      (v: list t')
      (item_match: (t -> v': t'{v' << v} -> vprop))
    : Tot vprop (decreases v)

    c: FStar.Seq.Base.seq t ->
    v: Prims.list t' ->
    item_match: (_: t -> v': t'{v' << v} -> Steel.Effect.Common.vprop)
  -> Prims.Tot Steel.Effect.Common.vprop