fsdoc: no-summary-found
fsdoc: no-comment-found
let ((write_at_end (#a:Type) (#i:rid) (r:m_rref i (seq a) grows) (x:a)):(ST unit ((requires ((fun h -> True)))) ((ensures ((fun h0 _ h1 -> /\(/\(/\(/\(contains h1 r, modifies_one i h0 h1), modifies_ref i (Set.singleton (HS.as_addr r)) h0 h1), ==(HS.sel h1 r, Seq.snoc (HS.sel h0 r) x)), witnessed (at_least (Seq.length (HS.sel h0 r)) x r)))))))):recall r; let s0 = !(r) in let n = Seq.length s0 in :=(r, Seq.snoc s0 x); at_least_is_stable n x r; Seq.contains_snoc s0 x; mr_witness r (at_least n x r)extending a stored sequence, witnessing its new entry for convenience.
val collect:Unidentified product: [(Unidentified product: ['a] (Tot (seq 'b)))] Unidentified product: [s:seq 'a] (Tot (seq 'b) (decreases (Seq.length s)))yields the concatenation of all sequences returned by f applied to the sequence elements