val to_lseq (#a: Type0) (s: seq a {length s <= max_size_t}) : l: lseq a (length s) {l == s}
let to_lseq (#a:Type0) (s:seq a{length s <= max_size_t}) : l:lseq a (length s){l == s} = s
val to_lseq (#a: Type0) (s: seq a {length s <= max_size_t}) : l: lseq a (length s) {l == s}
let to_lseq (#a: Type0) (s: seq a {length s <= max_size_t}) : l: lseq a (length s) {l == s} =
s
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.Sequence.seq Prims.b2t Prims.op_LessThanOrEqual Lib.Sequence.length Lib.IntTypes.max_size_t Lib.Sequence.lseq Prims.eq2 Prims.l_or Prims.nat FStar.Seq.Base.length
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}
val to_lseq (#a: Type0) (s: seq a {length s <= max_size_t}) : l: lseq a (length s) {l == s}
s: Lib.Sequence.seq a {Lib.Sequence.length s <= Lib.IntTypes.max_size_t}
  -> l: Lib.Sequence.lseq a (Lib.Sequence.length s) {l == s}