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)})
let create #a len init = Seq.create #a len init
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)})
let create #a len init =
Seq.create #a len init
Lib.Sequence.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.Properties.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 FStar.Calc.fsti.checked
Lib.Sequence.fst
Lib.IntTypes.size_nat FStar.Seq.Base.create Lib.Sequence.lseq Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Lib.Sequence.index
module Lib.Sequence

open FStar.Mul
open Lib.IntTypes
open Lib.LoopCombinators

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

let index #a #len s n = Seq.index s n
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)})
len: Lib.IntTypes.size_nat -> init: a
  -> s:
    Lib.Sequence.lseq a len
      { Lib.Sequence.to_seq s == FStar.Seq.Base.create len init /\
        (forall (i: Prims.nat). {:pattern Lib.Sequence.index s i}
            i < len ==> Lib.Sequence.index s i == init) }