val length (#a: Type0) (s: seq a) : nat
let length (#a:Type0) (s:seq a) : nat = Seq.length s
val length (#a: Type0) (s: seq a) : nat
let length (#a: Type0) (s: seq a) : nat =
Seq.length 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 FStar.Seq.Base.length Prims.nat
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
val length (#a: Type0) (s: seq a) : nat
s: Lib.Sequence.seq a -> Prims.nat