val singleton (x: 'a) : Tot (Seq.seq 'a)
val singleton (x: 'a) : Tot (Seq.seq 'a)
let singleton (x:'a) : Tot (Seq.seq 'a) = Seq.create 1 x
module MiTLS.StreamDeltas
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open FStar.HyperStack
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module HS   = FStar.HyperStack
module HST = FStar.HyperStack.ST //Added automatically; avoid.
module MS   = FStar.Monotonic.Seq
module S    = MiTLS.StAE
module C    = MiTLS.Content
module DS   = MiTLS.DataStream

let deltas i = Seq.seq (DS.delta i) //not yet handling the well-formedness condition of final deltas
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StAE.fst.checked MiTLS.Mem.fst.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
MiTLS.StreamDeltas.fst
x: 'a -> FStar.Seq.Base.seq 'a
FStar.Seq.Base.create FStar.Seq.Base.seq
let singleton (x: 'a) : Tot (Seq.seq 'a) =
  
Seq.create 1 x