package fstar
-
fstar.lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type ('a, 's1, 's2) grows_aux = Prims.unittype ('a, 'uuuuu, 'uuuuu1) grows = Prims.unittype rid = Prims.unitval snoc : 'a FStar_Seq_Base.seq -> 'a -> 'a FStar_Seq_Base.seqval alloc_mref_seq :
Prims.unit ->
'a FStar_Seq_Base.seq ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.reftype ('a, 'i, 'n, 'x, 'r, 'h) at_least = Prims.unitval write_at_end :
Prims.unit ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref ->
'a ->
Prims.unittype ('a, 'p, 's1, 's2) grows_p = Prims.unittype ('r, !'a, 'p) i_seq =
(Prims.unit, 'a FStar_Seq_Base.seq, Prims.unit) FStar_HyperStack_ST.m_rrefval alloc_mref_iseq :
Prims.unit ->
'a FStar_Seq_Base.seq ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.reftype ('r, 'a, 'p, 'n, 'x, 'm, 'h) i_at_least = Prims.unittype ('r, 'a, 'p, 'x, 'is, 'h) int_at_most = Prims.unitval i_read :
Prims.unit ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref ->
'a FStar_Seq_Base.seqtype ('r, 'a, 'p, 'm, 'h) i_contains = Prims.unitval i_write_at_end :
Prims.unit ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref ->
'a ->
Prims.unittype 's invariant = Prims.unitval test0 :
Prims.unit ->
(Prims.unit,
Prims.nat FStar_Seq_Base.seq,
(Prims.nat, Prims.unit, Prims.unit) grows)
FStar_HyperStack_ST.m_rref ->
Prims.nat ->
Prims.unitval itest :
Prims.unit ->
(Prims.unit, Prims.nat, Prims.unit invariant) i_seq ->
Prims.nat ->
Prims.unitval un_snoc : 'a FStar_Seq_Base.seq -> 'a FStar_Seq_Base.seq * 'aval map : ('a -> 'b) -> 'a FStar_Seq_Base.seq -> 'b FStar_Seq_Base.seqval op_At :
'uuuuu FStar_Seq_Base.seq ->
'uuuuu FStar_Seq_Base.seq ->
'uuuuu FStar_Seq_Base.seqtype ('a, 'b, 'i, 'r, 'f, 'bs, 'h) map_prefix = Prims.unittype ('a, 'b, 'i, 'r, 'f, 'n, 'v, 'h) map_has_at_index = Prims.unitval collect :
('a -> 'b FStar_Seq_Base.seq) ->
'a FStar_Seq_Base.seq ->
'b FStar_Seq_Base.seqtype ('a, 'b, 'i, 'r, 'f, 'bs, 'h) collect_prefix = Prims.unittype ('a, 'b, 'i, 'r, 'f, 'n, 'v, 'h) collect_has_at_index = Prims.unittype ('i, !'a) log_t =
(Prims.unit, 'a FStar_Seq_Base.seq, Prims.unit) FStar_HyperStack_ST.m_rreftype ('x, 'y) increases = Prims.unittype ('l, 'a, 'x, 'log, 'h) at_most_log_len = Prims.unittype ('l, 'a, 'i, 'log, 'max) seqn_val = Prims.nattype ('l, 'a, 'i, 'log, 'max) seqn =
(Prims.unit,
(Prims.unit, 'a, Prims.unit, Prims.unit, Prims.unit) seqn_val,
Prims.unit)
FStar_HyperStack_ST.m_rrefval new_seqn :
Prims.unit ->
Prims.nat ->
Prims.unit ->
Prims.nat ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref ->
Prims.nat FStar_HyperStack_ST.refval increment_seqn :
Prims.unit ->
Prims.nat ->
Prims.unit ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref ->
Prims.nat FStar_HyperStack_ST.ref ->
Prims.unitval testify_seqn :
Prims.unit ->
Prims.unit ->
'a FStar_Seq_Base.seq FStar_HyperStack_ST.ref ->
Prims.nat ->
Prims.nat FStar_HyperStack_ST.ref ->
Prims.unit