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 'n fin = Prims.inttype 'p under = Prims.nattype ('n, !'a) vect = 'a Prims.listtype ('n, !'a) seqn = 'a FStar_Seq_Base.seqtype ('a, 's) in_ = Prims.natval find :
'a FStar_Seq_Base.seq ->
('a -> Prims.bool) ->
Prims.nat ->
Prims.nat FStar_Pervasives_Native.optionval pigeonhole :
Prims.pos ->
Prims.nat FStar_Seq_Base.seq ->
Prims.nat * Prims.nattype !'a binary_relation = 'a -> 'a -> Prims.booltype ('a, 'r) is_reflexive = Prims.unittype ('a, 'r) is_symmetric = Prims.unittype ('a, 'r) is_transitive = Prims.unittype !'a equivalence_relation = 'a -> 'a -> Prims.booltype ('a, 'eq, 's, 'x) contains_eq = Prims.unitval find_eq :
'a equivalence_relation ->
'a FStar_Seq_Base.seq ->
'a ->
Prims.natval pigeonhole_eq :
'a equivalence_relation ->
'a FStar_Seq_Base.seq ->
'a FStar_Seq_Base.seq ->
Prims.nat * Prims.nat