val seq_list_match_nil0 (#t: Type) (c: Seq.seq t) : Tot vprop
let seq_list_match_nil0
  (#t: Type)
  (c: Seq.seq t)
: Tot vprop
= pure (c `Seq.equal` Seq.empty)
val seq_list_match_nil0 (#t: Type) (c: Seq.seq t) : Tot vprop
let seq_list_match_nil0 (#t: Type) (c: Seq.seq t) : Tot vprop =
pure (c `Seq.equal` Seq.empty)
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 Steel.ST.Util.pure FStar.Seq.Base.equal FStar.Seq.Base.empty Steel.Effect.Common.vprop
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)
val seq_list_match_nil0 (#t: Type) (c: Seq.seq t) : Tot vprop
c: FStar.Seq.Base.seq t -> Steel.Effect.Common.vprop