val to_seq (#a: Type0) (#len: size_nat) (l: lseq a len) : seq a
let to_seq (#a:Type0) (#len:size_nat) (l:lseq a len) : seq a = l
val to_seq (#a: Type0) (#len: size_nat) (l: lseq a len) : seq a
let to_seq (#a: Type0) (#len: size_nat) (l: lseq a len) : seq a =
l
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 Lib.Sequence.lseq Lib.Sequence.seq
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 *)
val to_seq (#a: Type0) (#len: size_nat) (l: lseq a len) : seq a
l: Lib.Sequence.lseq a len -> Lib.Sequence.seq a