To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
fstar 2022.01.15
Libraries
This package provides the following libraries (via ocamlobjinfo):
fstarlib
Documentation:
PrimsFStar_Algebra_CommMonoidFStar_Algebra_CommMonoid_EquivFStar_Pervasives_NativeFStar_Algebra_MonoidFStar_AllFStar_Monotonic_HeapFStar_CommonSTFStar_STFStar_RefFStar_List_Tot_BaseFStar_Seq_BaseFStar_Seq_PropertiesFStar_ArrayFStar_HeapFStar_Axiomatic_ArrayFStar_BitVectorFStar_UIntFStar_BVFStar_UInt32FStar_CharFStar_FloatFStar_Int16FStar_Int32FStar_Int64FStar_Int8FStar_UInt16FStar_UInt8FStar_BaseTypesFStar_BigOpsFStar_UInt64FStar_IntFStar_Int_CastFStar_UInt128FStar_BufferFStar_BytesFStar_CalcFStar_ClassicalFStar_Classical_SugarFStar_IFCFStar_Int128FStar_IntegersFStar_ConstantTime_IntegersFStar_PervasivesFStar_ConstructiveFStar_CryptoFStar_DateFStar_FunctionalExtensionalityFStar_DependentMapFStar_DynFStar_EndiannessFStar_ErasedLogicFStar_ErrorFStar_ExnFStar_FinFStar_GSetFStar_GhostFStar_SetFStar_MapFStar_Monotonic_HyperHeapFStar_Monotonic_HyperStackFStar_HyperStackFStar_HyperStack_AllFStar_IOFStar_HyperStack_IOFStar_HyperStack_STFStar_IndefiniteDescriptionFStar_Int_Cast_FullFStar_WellFoundedFStar_LexicographicOrderingFStar_ListFStar_List_Tot_PropertiesFStar_MRefFStar_MarkovsPrincipleFStar_Math_EuclidFStar_Math_FermatFStar_Math_LemmasFStar_Math_LibFStar_UniverseFStar_ModifiesGenFStar_ModifiesFStar_Monotonic_DependentMapFStar_Monotonic_MapFStar_Monotonic_PureFStar_Monotonic_SeqFStar_Monotonic_WitnessedFStar_MulFStar_OptionFStar_OrdSetFStar_OrdMapFStar_OrdMapPropsFStar_OrdSetPropsFStar_PCMFStar_PartialMapFStar_PointerFStar_StringFStar_Pointer_BaseFStar_PredicateExtensionalityFStar_PreorderFStar_PropositionalExtensionalityFStar_ReflexiveTransitiveClosureFStar_Relational_RelationalFStar_Relational_CompFStar_Relational_StateFStar_SeqFStar_Seq_PermutationFStar_Seq_SortedFStar_SequenceFStar_Sequence_AmbientFStar_Sequence_BaseFStar_Sequence_UtilFStar_Sequence_PermutationFStar_Sequence_SeqFStar_SquashFStar_SquashPropertiesFStar_StrongExcludedMiddleFStar_TcpFStar_TwoLevelHeapFStar_UdpFStar_Universe_PCMLowStar_Monotonic_BufferLowStar_BufferLowStar_BufferCompatLowStar_BufferOpsLowStar_BufferViewLowStar_BufferView_DownLowStar_BufferView_UpLowStar_CommentLowStar_ImmutableBufferLowStar_ConstBufferLowStar_EndiannessLowStar_ModifiesLowStar_ModifiesPatLowStar_PrefixFreezableBufferLowStar_RegionalLowStar_VectorLowStar_RVectorLowStar_Regional_InstancesLowStar_ToFStarBufferLowStar_UninitializedBufferSteel_CommonSteel_EffectSteel_HigherReferenceSteel_MonotonicHigherReferenceSteel_Primitive_ForkJoinSteel_ReferenceSteel_SpinLock
fstartaclib
Documentation:
FStar_Algebra_CommMonoidFStar_Algebra_CommMonoid_EquivFStar_Algebra_MonoidFStar_AllFStar_RefFStar_Seq_BaseFStar_Seq_PropertiesFStar_ArrayFStar_HeapFStar_Axiomatic_ArrayFStar_BitVectorFStar_UIntFStar_BVFStar_BigOpsFStar_IntFStar_UInt64FStar_Int_CastFStar_UInt128FStar_BufferFStar_BytesFStar_CalcFStar_ClassicalFStar_Classical_SugarFStar_IFCFStar_Int128FStar_IntegersFStar_ConstantTime_IntegersFStar_ConstructiveFStar_CryptoFStar_DateFStar_FunctionalExtensionalityFStar_DependentMapFStar_DynFStar_EndiannessFStar_ErasedLogicFStar_ErrorFStar_ExnFStar_FinFStar_GSetFStar_GhostFStar_SetFStar_MapFStar_Monotonic_HyperHeapFStar_Monotonic_HyperStackFStar_HyperStackFStar_HyperStack_AllFStar_IOFStar_HyperStack_IOFStar_HyperStack_STFStar_IndefiniteDescriptionFStar_Int_Cast_FullFStar_InteractiveHelpersFStar_RangeFStar_Reflection_BuiltinsFStar_Reflection_TypesFStar_Tactics_EffectFStar_Tactics_BuiltinsFStar_Reflection_ConstFStar_Reflection_DerivedFStar_Reflection_FormulaFStar_Tactics_SyntaxHelpersFStar_Tactics_UtilFStar_Tactics_DerivedFStar_InteractiveHelpers_BaseFStar_InteractiveHelpers_ExploreTermFStar_InteractiveHelpers_PropositionsFStar_InteractiveHelpers_EffectfulFStar_InteractiveHelpers_OutputFStar_InteractiveHelpers_PostProcessFStar_WellFoundedFStar_LexicographicOrderingFStar_List_Tot_PropertiesFStar_MRefFStar_MarkovsPrincipleFStar_Math_EuclidFStar_Math_FermatFStar_Math_LemmasFStar_Math_LibFStar_UniverseFStar_ModifiesGenFStar_ModifiesFStar_Monotonic_DependentMapFStar_Monotonic_MapFStar_Monotonic_PureFStar_Monotonic_SeqFStar_Monotonic_WitnessedFStar_MulFStar_OptionFStar_OrdSetFStar_OrdMapFStar_OrdMapPropsFStar_OrdSetPropsFStar_PCMFStar_PartialMapFStar_PointerFStar_Pointer_BaseFStar_PredicateExtensionalityFStar_PreorderFStar_PropositionalExtensionalityFStar_ReflectionFStar_Reflection_Derived_LemmasFStar_Reflection_ArithFStar_ReflexiveTransitiveClosureFStar_Relational_RelationalFStar_Relational_CompFStar_Relational_StateFStar_SeqFStar_Seq_PermutationFStar_Seq_SortedFStar_SequenceFStar_Sequence_AmbientFStar_Sequence_BaseFStar_Sequence_UtilFStar_Sequence_PermutationFStar_Sequence_SeqFStar_SquashFStar_SquashPropertiesFStar_StrongExcludedMiddleFStar_TacticsFStar_Tactics_LogicFStar_Tactics_ArithFStar_Tactics_BVFStar_Tactics_CanonFStar_Tactics_CanonCommMonoidFStar_Tactics_CanonCommMonoidSimpleFStar_Tactics_CanonCommMonoidSimple_EquivFStar_Tactics_CanonCommSemiringFStar_Tactics_CanonCommSwapsFStar_Tactics_CanonMonoidFStar_Tactics_PatternMatchingFStar_Tactics_PrintFStar_Tactics_SimplifierFStar_Tactics_TypeclassesFStar_TcpFStar_TwoLevelHeapFStar_UdpFStar_Universe_PCMLowStar_Monotonic_BufferLowStar_BufferLowStar_BufferCompatLowStar_BufferOpsLowStar_BufferViewLowStar_BufferView_DownLowStar_BufferView_UpLowStar_CommentLowStar_ImmutableBufferLowStar_ConstBufferLowStar_EndiannessLowStar_ModifiesLowStar_ModifiesPatLowStar_PrefixFreezableBufferLowStar_RegionalLowStar_VectorLowStar_RVectorLowStar_Regional_InstancesLowStar_ToFStarBufferLowStar_UninitializedBufferSteel_Effect_Common
fstartaclib
Documentation:
FStar_Algebra_CommMonoidFStar_Algebra_CommMonoid_EquivFStar_Algebra_MonoidFStar_AllFStar_RefFStar_Seq_BaseFStar_Seq_PropertiesFStar_ArrayFStar_HeapFStar_Axiomatic_ArrayFStar_BitVectorFStar_UIntFStar_BVFStar_BigOpsFStar_IntFStar_UInt64FStar_Int_CastFStar_UInt128FStar_BufferFStar_BytesFStar_CalcFStar_ClassicalFStar_Classical_SugarFStar_IFCFStar_Int128FStar_IntegersFStar_ConstantTime_IntegersFStar_ConstructiveFStar_CryptoFStar_DateFStar_FunctionalExtensionalityFStar_DependentMapFStar_DynFStar_EndiannessFStar_ErasedLogicFStar_ErrorFStar_ExnFStar_FinFStar_GSetFStar_GhostFStar_SetFStar_MapFStar_Monotonic_HyperHeapFStar_Monotonic_HyperStackFStar_HyperStackFStar_HyperStack_AllFStar_IOFStar_HyperStack_IOFStar_HyperStack_STFStar_IndefiniteDescriptionFStar_Int_Cast_FullFStar_InteractiveHelpersFStar_RangeFStar_Reflection_BuiltinsFStar_Reflection_TypesFStar_Tactics_EffectFStar_Tactics_BuiltinsFStar_Reflection_ConstFStar_Reflection_DerivedFStar_Reflection_FormulaFStar_Tactics_SyntaxHelpersFStar_Tactics_UtilFStar_Tactics_DerivedFStar_InteractiveHelpers_BaseFStar_InteractiveHelpers_ExploreTermFStar_InteractiveHelpers_PropositionsFStar_InteractiveHelpers_EffectfulFStar_InteractiveHelpers_OutputFStar_InteractiveHelpers_PostProcessFStar_WellFoundedFStar_LexicographicOrderingFStar_List_Tot_PropertiesFStar_MRefFStar_MarkovsPrincipleFStar_Math_EuclidFStar_Math_FermatFStar_Math_LemmasFStar_Math_LibFStar_UniverseFStar_ModifiesGenFStar_ModifiesFStar_Monotonic_DependentMapFStar_Monotonic_MapFStar_Monotonic_PureFStar_Monotonic_SeqFStar_Monotonic_WitnessedFStar_MulFStar_OptionFStar_OrdSetFStar_OrdMapFStar_OrdMapPropsFStar_OrdSetPropsFStar_PCMFStar_PartialMapFStar_PointerFStar_Pointer_BaseFStar_PredicateExtensionalityFStar_PreorderFStar_PropositionalExtensionalityFStar_ReflectionFStar_Reflection_Derived_LemmasFStar_Reflection_ArithFStar_ReflexiveTransitiveClosureFStar_Relational_RelationalFStar_Relational_CompFStar_Relational_StateFStar_SeqFStar_Seq_PermutationFStar_Seq_SortedFStar_SequenceFStar_Sequence_AmbientFStar_Sequence_BaseFStar_Sequence_UtilFStar_Sequence_PermutationFStar_Sequence_SeqFStar_SquashFStar_SquashPropertiesFStar_StrongExcludedMiddleFStar_TacticsFStar_Tactics_LogicFStar_Tactics_ArithFStar_Tactics_BVFStar_Tactics_CanonFStar_Tactics_CanonCommMonoidFStar_Tactics_CanonCommMonoidSimpleFStar_Tactics_CanonCommMonoidSimple_EquivFStar_Tactics_CanonCommSemiringFStar_Tactics_CanonCommSwapsFStar_Tactics_CanonMonoidFStar_Tactics_PatternMatchingFStar_Tactics_PrintFStar_Tactics_SimplifierFStar_Tactics_TypeclassesFStar_TcpFStar_TwoLevelHeapFStar_UdpFStar_Universe_PCMLowStar_Monotonic_BufferLowStar_BufferLowStar_BufferCompatLowStar_BufferOpsLowStar_BufferViewLowStar_BufferView_DownLowStar_BufferView_UpLowStar_CommentLowStar_ImmutableBufferLowStar_ConstBufferLowStar_EndiannessLowStar_ModifiesLowStar_ModifiesPatLowStar_PrefixFreezableBufferLowStar_RegionalLowStar_VectorLowStar_RVectorLowStar_Regional_InstancesLowStar_ToFStarBufferLowStar_UninitializedBufferSteel_Effect_Common
fstarlib
Documentation:
PrimsFStar_Algebra_CommMonoidFStar_Algebra_CommMonoid_EquivFStar_Pervasives_NativeFStar_Algebra_MonoidFStar_AllFStar_Monotonic_HeapFStar_CommonSTFStar_STFStar_RefFStar_List_Tot_BaseFStar_Seq_BaseFStar_Seq_PropertiesFStar_ArrayFStar_HeapFStar_Axiomatic_ArrayFStar_BitVectorFStar_UIntFStar_BVFStar_UInt32FStar_CharFStar_FloatFStar_Int16FStar_Int32FStar_Int64FStar_Int8FStar_UInt16FStar_UInt8FStar_BaseTypesFStar_BigOpsFStar_UInt64FStar_IntFStar_Int_CastFStar_UInt128FStar_BufferFStar_BytesFStar_CalcFStar_ClassicalFStar_Classical_SugarFStar_IFCFStar_Int128FStar_IntegersFStar_ConstantTime_IntegersFStar_PervasivesFStar_ConstructiveFStar_CryptoFStar_DateFStar_FunctionalExtensionalityFStar_DependentMapFStar_DynFStar_EndiannessFStar_ErasedLogicFStar_ErrorFStar_ExnFStar_FinFStar_GSetFStar_GhostFStar_SetFStar_MapFStar_Monotonic_HyperHeapFStar_Monotonic_HyperStackFStar_HyperStackFStar_HyperStack_AllFStar_IOFStar_HyperStack_IOFStar_HyperStack_STFStar_IndefiniteDescriptionFStar_Int_Cast_FullFStar_WellFoundedFStar_LexicographicOrderingFStar_ListFStar_List_Tot_PropertiesFStar_MRefFStar_MarkovsPrincipleFStar_Math_EuclidFStar_Math_FermatFStar_Math_LemmasFStar_Math_LibFStar_UniverseFStar_ModifiesGenFStar_ModifiesFStar_Monotonic_DependentMapFStar_Monotonic_MapFStar_Monotonic_PureFStar_Monotonic_SeqFStar_Monotonic_WitnessedFStar_MulFStar_OptionFStar_OrdSetFStar_OrdMapFStar_OrdMapPropsFStar_OrdSetPropsFStar_PCMFStar_PartialMapFStar_PointerFStar_StringFStar_Pointer_BaseFStar_PredicateExtensionalityFStar_PreorderFStar_PropositionalExtensionalityFStar_ReflexiveTransitiveClosureFStar_Relational_RelationalFStar_Relational_CompFStar_Relational_StateFStar_SeqFStar_Seq_PermutationFStar_Seq_SortedFStar_SequenceFStar_Sequence_AmbientFStar_Sequence_BaseFStar_Sequence_UtilFStar_Sequence_PermutationFStar_Sequence_SeqFStar_SquashFStar_SquashPropertiesFStar_StrongExcludedMiddleFStar_TcpFStar_TwoLevelHeapFStar_UdpFStar_Universe_PCMLowStar_Monotonic_BufferLowStar_BufferLowStar_BufferCompatLowStar_BufferOpsLowStar_BufferViewLowStar_BufferView_DownLowStar_BufferView_UpLowStar_CommentLowStar_ImmutableBufferLowStar_ConstBufferLowStar_EndiannessLowStar_ModifiesLowStar_ModifiesPatLowStar_PrefixFreezableBufferLowStar_RegionalLowStar_VectorLowStar_RVectorLowStar_Regional_InstancesLowStar_ToFStarBufferLowStar_UninitializedBufferSteel_CommonSteel_EffectSteel_HigherReferenceSteel_MonotonicHigherReferenceSteel_Primitive_ForkJoinSteel_ReferenceSteel_SpinLock
On This Page