let ( @| ) #a #len0 #len1 s0 s1 = concat #a #len0 #len1 s0 s1
let op_At_Bar #a #len0 #len1 s0 s1 =
concat #a #len0 #len1 s0 s1
Lib.Sequence.fsti.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked
Lib.Sequence.fsti
Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t Lib.Sequence.lseq Lib.Sequence.concat Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.append
module Lib.Sequence

open FStar.Mul
open Lib.IntTypes

#set-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 --using_facts_from '-* +Prims +FStar.Math.Lemmas +FStar.Seq +Lib.IntTypes +Lib.Sequence'"

/// Variable length Sequences, derived from FStar.Seq

(* This is the type of unbounded sequences.
   Use this only when dealing with, say, user input whose length is unbounded.
   As far as possible use the API for bounded sequences defined later in this file.*)

(** Definition of a Sequence *)
let seq (a:Type0) = Seq.seq a

(** Length of a Sequence *)
let length (#a:Type0) (s:seq a) : nat = Seq.length s

/// Fixed length Sequences

(* This is the type of bounded sequences.
   Use this as much as possible.
   It adds additional length checks that you'd have to prove in the implementation otherwise *)

(** Definition of a fixed-length Sequence *)
let lseq (a:Type0) (len:size_nat) = s:seq a{Seq.length s == len}
let to_seq (#a:Type0) (#len:size_nat) (l:lseq a len) : seq a = l
let to_lseq (#a:Type0) (s:seq a{length s <= max_size_t}) : l:lseq a (length s){l == s} = s

(* If you want to prove your code with an abstract lseq use the following: *)
// val lseq: a:Type0 -> len:size_nat -> Type0
// val to_seq: #a:Type0 -> #len:size_nat -> lseq a len -> s:seq a{length s == len}
// val to_lseq: #a:Type0 -> s:seq a{length s <= max_size_t} -> lseq a (length s)

val index:
    #a:Type
  -> #len:size_nat
  -> s:lseq a len
  -> i:size_nat{i < len} ->
  Tot (r:a{r == Seq.index (to_seq s) i})

(** Creation of a fixed-length Sequence from an initial value *)
val create:
    #a:Type
  -> len:size_nat
  -> init:a ->
  Tot (s:lseq a len{to_seq s == Seq.create len init /\ (forall (i:nat).
    {:pattern (index s i)} i < len ==> index s i == init)})


(** Concatenate sequences: use with care, may make implementation hard to verify *)
val concat:
    #a:Type
  -> #len0:size_nat
  -> #len1:size_nat{len0 + len1 <= max_size_t}
  -> s0:lseq a len0
  -> s1:lseq a len1 ->
  Tot (s2:lseq a (len0 + len1){to_seq s2 == Seq.append (to_seq s0) (to_seq s1)})
val op_At_Bar : s0: Lib.Sequence.lseq a len0 -> s1: Lib.Sequence.lseq a len1
  -> s2:
    Lib.Sequence.lseq a (len0 + len1)
      { Lib.Sequence.to_seq s2 ==
        FStar.Seq.Base.append (Lib.Sequence.to_seq s0) (Lib.Sequence.to_seq s1) }
s0: Lib.Sequence.lseq a len0 -> s1: Lib.Sequence.lseq a len1
  -> s2:
    Lib.Sequence.lseq a (len0 + len1)
      { Lib.Sequence.to_seq s2 ==
        FStar.Seq.Base.append (Lib.Sequence.to_seq s0) (Lib.Sequence.to_seq s1) }