To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
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:
Prims
FStar_Algebra_CommMonoid
FStar_Algebra_CommMonoid_Equiv
FStar_Pervasives_Native
FStar_Algebra_Monoid
FStar_All
FStar_Monotonic_Heap
FStar_CommonST
FStar_ST
FStar_Ref
FStar_List_Tot_Base
FStar_Seq_Base
FStar_Seq_Properties
FStar_Array
FStar_Heap
FStar_Axiomatic_Array
FStar_BitVector
FStar_UInt
FStar_BV
FStar_UInt32
FStar_Char
FStar_Float
FStar_Int16
FStar_Int32
FStar_Int64
FStar_Int8
FStar_UInt16
FStar_UInt8
FStar_BaseTypes
FStar_BigOps
FStar_UInt64
FStar_Int
FStar_Int_Cast
FStar_UInt128
FStar_Buffer
FStar_Bytes
FStar_Calc
FStar_Classical
FStar_Classical_Sugar
FStar_IFC
FStar_Int128
FStar_Integers
FStar_ConstantTime_Integers
FStar_Pervasives
FStar_Constructive
FStar_Crypto
FStar_Date
FStar_FunctionalExtensionality
FStar_DependentMap
FStar_Dyn
FStar_Endianness
FStar_ErasedLogic
FStar_Error
FStar_Exn
FStar_Fin
FStar_GSet
FStar_Ghost
FStar_Set
FStar_Map
FStar_Monotonic_HyperHeap
FStar_Monotonic_HyperStack
FStar_HyperStack
FStar_HyperStack_All
FStar_IO
FStar_HyperStack_IO
FStar_HyperStack_ST
FStar_IndefiniteDescription
FStar_Int_Cast_Full
FStar_WellFounded
FStar_LexicographicOrdering
FStar_List
FStar_List_Tot_Properties
FStar_MRef
FStar_MarkovsPrinciple
FStar_Math_Euclid
FStar_Math_Fermat
FStar_Math_Lemmas
FStar_Math_Lib
FStar_Universe
FStar_ModifiesGen
FStar_Modifies
FStar_Monotonic_DependentMap
FStar_Monotonic_Map
FStar_Monotonic_Pure
FStar_Monotonic_Seq
FStar_Monotonic_Witnessed
FStar_Mul
FStar_Option
FStar_OrdSet
FStar_OrdMap
FStar_OrdMapProps
FStar_OrdSetProps
FStar_PCM
FStar_PartialMap
FStar_Pointer
FStar_String
FStar_Pointer_Base
FStar_PredicateExtensionality
FStar_Preorder
FStar_PropositionalExtensionality
FStar_ReflexiveTransitiveClosure
FStar_Relational_Relational
FStar_Relational_Comp
FStar_Relational_State
FStar_Seq
FStar_Seq_Permutation
FStar_Seq_Sorted
FStar_Sequence
FStar_Sequence_Ambient
FStar_Sequence_Base
FStar_Sequence_Util
FStar_Sequence_Permutation
FStar_Sequence_Seq
FStar_Squash
FStar_SquashProperties
FStar_StrongExcludedMiddle
FStar_Tcp
FStar_TwoLevelHeap
FStar_Udp
FStar_Universe_PCM
LowStar_Monotonic_Buffer
LowStar_Buffer
LowStar_BufferCompat
LowStar_BufferOps
LowStar_BufferView
LowStar_BufferView_Down
LowStar_BufferView_Up
LowStar_Comment
LowStar_ImmutableBuffer
LowStar_ConstBuffer
LowStar_Endianness
LowStar_Modifies
LowStar_ModifiesPat
LowStar_PrefixFreezableBuffer
LowStar_Regional
LowStar_Vector
LowStar_RVector
LowStar_Regional_Instances
LowStar_ToFStarBuffer
LowStar_UninitializedBuffer
Steel_Common
Steel_Effect
Steel_HigherReference
Steel_MonotonicHigherReference
Steel_Primitive_ForkJoin
Steel_Reference
Steel_SpinLock
fstartaclib
Documentation:
FStar_Algebra_CommMonoid
FStar_Algebra_CommMonoid_Equiv
FStar_Algebra_Monoid
FStar_All
FStar_Ref
FStar_Seq_Base
FStar_Seq_Properties
FStar_Array
FStar_Heap
FStar_Axiomatic_Array
FStar_BitVector
FStar_UInt
FStar_BV
FStar_BigOps
FStar_Int
FStar_UInt64
FStar_Int_Cast
FStar_UInt128
FStar_Buffer
FStar_Bytes
FStar_Calc
FStar_Classical
FStar_Classical_Sugar
FStar_IFC
FStar_Int128
FStar_Integers
FStar_ConstantTime_Integers
FStar_Constructive
FStar_Crypto
FStar_Date
FStar_FunctionalExtensionality
FStar_DependentMap
FStar_Dyn
FStar_Endianness
FStar_ErasedLogic
FStar_Error
FStar_Exn
FStar_Fin
FStar_GSet
FStar_Ghost
FStar_Set
FStar_Map
FStar_Monotonic_HyperHeap
FStar_Monotonic_HyperStack
FStar_HyperStack
FStar_HyperStack_All
FStar_IO
FStar_HyperStack_IO
FStar_HyperStack_ST
FStar_IndefiniteDescription
FStar_Int_Cast_Full
FStar_InteractiveHelpers
FStar_Range
FStar_Reflection_Builtins
FStar_Reflection_Types
FStar_Tactics_Effect
FStar_Tactics_Builtins
FStar_Reflection_Const
FStar_Reflection_Derived
FStar_Reflection_Formula
FStar_Tactics_SyntaxHelpers
FStar_Tactics_Util
FStar_Tactics_Derived
FStar_InteractiveHelpers_Base
FStar_InteractiveHelpers_ExploreTerm
FStar_InteractiveHelpers_Propositions
FStar_InteractiveHelpers_Effectful
FStar_InteractiveHelpers_Output
FStar_InteractiveHelpers_PostProcess
FStar_WellFounded
FStar_LexicographicOrdering
FStar_List_Tot_Properties
FStar_MRef
FStar_MarkovsPrinciple
FStar_Math_Euclid
FStar_Math_Fermat
FStar_Math_Lemmas
FStar_Math_Lib
FStar_Universe
FStar_ModifiesGen
FStar_Modifies
FStar_Monotonic_DependentMap
FStar_Monotonic_Map
FStar_Monotonic_Pure
FStar_Monotonic_Seq
FStar_Monotonic_Witnessed
FStar_Mul
FStar_Option
FStar_OrdSet
FStar_OrdMap
FStar_OrdMapProps
FStar_OrdSetProps
FStar_PCM
FStar_PartialMap
FStar_Pointer
FStar_Pointer_Base
FStar_PredicateExtensionality
FStar_Preorder
FStar_PropositionalExtensionality
FStar_Reflection
FStar_Reflection_Derived_Lemmas
FStar_Reflection_Arith
FStar_ReflexiveTransitiveClosure
FStar_Relational_Relational
FStar_Relational_Comp
FStar_Relational_State
FStar_Seq
FStar_Seq_Permutation
FStar_Seq_Sorted
FStar_Sequence
FStar_Sequence_Ambient
FStar_Sequence_Base
FStar_Sequence_Util
FStar_Sequence_Permutation
FStar_Sequence_Seq
FStar_Squash
FStar_SquashProperties
FStar_StrongExcludedMiddle
FStar_Tactics
FStar_Tactics_Logic
FStar_Tactics_Arith
FStar_Tactics_BV
FStar_Tactics_Canon
FStar_Tactics_CanonCommMonoid
FStar_Tactics_CanonCommMonoidSimple
FStar_Tactics_CanonCommMonoidSimple_Equiv
FStar_Tactics_CanonCommSemiring
FStar_Tactics_CanonCommSwaps
FStar_Tactics_CanonMonoid
FStar_Tactics_PatternMatching
FStar_Tactics_Print
FStar_Tactics_Simplifier
FStar_Tactics_Typeclasses
FStar_Tcp
FStar_TwoLevelHeap
FStar_Udp
FStar_Universe_PCM
LowStar_Monotonic_Buffer
LowStar_Buffer
LowStar_BufferCompat
LowStar_BufferOps
LowStar_BufferView
LowStar_BufferView_Down
LowStar_BufferView_Up
LowStar_Comment
LowStar_ImmutableBuffer
LowStar_ConstBuffer
LowStar_Endianness
LowStar_Modifies
LowStar_ModifiesPat
LowStar_PrefixFreezableBuffer
LowStar_Regional
LowStar_Vector
LowStar_RVector
LowStar_Regional_Instances
LowStar_ToFStarBuffer
LowStar_UninitializedBuffer
Steel_Effect_Common
fstartaclib
Documentation:
FStar_Algebra_CommMonoid
FStar_Algebra_CommMonoid_Equiv
FStar_Algebra_Monoid
FStar_All
FStar_Ref
FStar_Seq_Base
FStar_Seq_Properties
FStar_Array
FStar_Heap
FStar_Axiomatic_Array
FStar_BitVector
FStar_UInt
FStar_BV
FStar_BigOps
FStar_Int
FStar_UInt64
FStar_Int_Cast
FStar_UInt128
FStar_Buffer
FStar_Bytes
FStar_Calc
FStar_Classical
FStar_Classical_Sugar
FStar_IFC
FStar_Int128
FStar_Integers
FStar_ConstantTime_Integers
FStar_Constructive
FStar_Crypto
FStar_Date
FStar_FunctionalExtensionality
FStar_DependentMap
FStar_Dyn
FStar_Endianness
FStar_ErasedLogic
FStar_Error
FStar_Exn
FStar_Fin
FStar_GSet
FStar_Ghost
FStar_Set
FStar_Map
FStar_Monotonic_HyperHeap
FStar_Monotonic_HyperStack
FStar_HyperStack
FStar_HyperStack_All
FStar_IO
FStar_HyperStack_IO
FStar_HyperStack_ST
FStar_IndefiniteDescription
FStar_Int_Cast_Full
FStar_InteractiveHelpers
FStar_Range
FStar_Reflection_Builtins
FStar_Reflection_Types
FStar_Tactics_Effect
FStar_Tactics_Builtins
FStar_Reflection_Const
FStar_Reflection_Derived
FStar_Reflection_Formula
FStar_Tactics_SyntaxHelpers
FStar_Tactics_Util
FStar_Tactics_Derived
FStar_InteractiveHelpers_Base
FStar_InteractiveHelpers_ExploreTerm
FStar_InteractiveHelpers_Propositions
FStar_InteractiveHelpers_Effectful
FStar_InteractiveHelpers_Output
FStar_InteractiveHelpers_PostProcess
FStar_WellFounded
FStar_LexicographicOrdering
FStar_List_Tot_Properties
FStar_MRef
FStar_MarkovsPrinciple
FStar_Math_Euclid
FStar_Math_Fermat
FStar_Math_Lemmas
FStar_Math_Lib
FStar_Universe
FStar_ModifiesGen
FStar_Modifies
FStar_Monotonic_DependentMap
FStar_Monotonic_Map
FStar_Monotonic_Pure
FStar_Monotonic_Seq
FStar_Monotonic_Witnessed
FStar_Mul
FStar_Option
FStar_OrdSet
FStar_OrdMap
FStar_OrdMapProps
FStar_OrdSetProps
FStar_PCM
FStar_PartialMap
FStar_Pointer
FStar_Pointer_Base
FStar_PredicateExtensionality
FStar_Preorder
FStar_PropositionalExtensionality
FStar_Reflection
FStar_Reflection_Derived_Lemmas
FStar_Reflection_Arith
FStar_ReflexiveTransitiveClosure
FStar_Relational_Relational
FStar_Relational_Comp
FStar_Relational_State
FStar_Seq
FStar_Seq_Permutation
FStar_Seq_Sorted
FStar_Sequence
FStar_Sequence_Ambient
FStar_Sequence_Base
FStar_Sequence_Util
FStar_Sequence_Permutation
FStar_Sequence_Seq
FStar_Squash
FStar_SquashProperties
FStar_StrongExcludedMiddle
FStar_Tactics
FStar_Tactics_Logic
FStar_Tactics_Arith
FStar_Tactics_BV
FStar_Tactics_Canon
FStar_Tactics_CanonCommMonoid
FStar_Tactics_CanonCommMonoidSimple
FStar_Tactics_CanonCommMonoidSimple_Equiv
FStar_Tactics_CanonCommSemiring
FStar_Tactics_CanonCommSwaps
FStar_Tactics_CanonMonoid
FStar_Tactics_PatternMatching
FStar_Tactics_Print
FStar_Tactics_Simplifier
FStar_Tactics_Typeclasses
FStar_Tcp
FStar_TwoLevelHeap
FStar_Udp
FStar_Universe_PCM
LowStar_Monotonic_Buffer
LowStar_Buffer
LowStar_BufferCompat
LowStar_BufferOps
LowStar_BufferView
LowStar_BufferView_Down
LowStar_BufferView_Up
LowStar_Comment
LowStar_ImmutableBuffer
LowStar_ConstBuffer
LowStar_Endianness
LowStar_Modifies
LowStar_ModifiesPat
LowStar_PrefixFreezableBuffer
LowStar_Regional
LowStar_Vector
LowStar_RVector
LowStar_Regional_Instances
LowStar_ToFStarBuffer
LowStar_UninitializedBuffer
Steel_Effect_Common
fstarlib
Documentation:
Prims
FStar_Algebra_CommMonoid
FStar_Algebra_CommMonoid_Equiv
FStar_Pervasives_Native
FStar_Algebra_Monoid
FStar_All
FStar_Monotonic_Heap
FStar_CommonST
FStar_ST
FStar_Ref
FStar_List_Tot_Base
FStar_Seq_Base
FStar_Seq_Properties
FStar_Array
FStar_Heap
FStar_Axiomatic_Array
FStar_BitVector
FStar_UInt
FStar_BV
FStar_UInt32
FStar_Char
FStar_Float
FStar_Int16
FStar_Int32
FStar_Int64
FStar_Int8
FStar_UInt16
FStar_UInt8
FStar_BaseTypes
FStar_BigOps
FStar_UInt64
FStar_Int
FStar_Int_Cast
FStar_UInt128
FStar_Buffer
FStar_Bytes
FStar_Calc
FStar_Classical
FStar_Classical_Sugar
FStar_IFC
FStar_Int128
FStar_Integers
FStar_ConstantTime_Integers
FStar_Pervasives
FStar_Constructive
FStar_Crypto
FStar_Date
FStar_FunctionalExtensionality
FStar_DependentMap
FStar_Dyn
FStar_Endianness
FStar_ErasedLogic
FStar_Error
FStar_Exn
FStar_Fin
FStar_GSet
FStar_Ghost
FStar_Set
FStar_Map
FStar_Monotonic_HyperHeap
FStar_Monotonic_HyperStack
FStar_HyperStack
FStar_HyperStack_All
FStar_IO
FStar_HyperStack_IO
FStar_HyperStack_ST
FStar_IndefiniteDescription
FStar_Int_Cast_Full
FStar_WellFounded
FStar_LexicographicOrdering
FStar_List
FStar_List_Tot_Properties
FStar_MRef
FStar_MarkovsPrinciple
FStar_Math_Euclid
FStar_Math_Fermat
FStar_Math_Lemmas
FStar_Math_Lib
FStar_Universe
FStar_ModifiesGen
FStar_Modifies
FStar_Monotonic_DependentMap
FStar_Monotonic_Map
FStar_Monotonic_Pure
FStar_Monotonic_Seq
FStar_Monotonic_Witnessed
FStar_Mul
FStar_Option
FStar_OrdSet
FStar_OrdMap
FStar_OrdMapProps
FStar_OrdSetProps
FStar_PCM
FStar_PartialMap
FStar_Pointer
FStar_String
FStar_Pointer_Base
FStar_PredicateExtensionality
FStar_Preorder
FStar_PropositionalExtensionality
FStar_ReflexiveTransitiveClosure
FStar_Relational_Relational
FStar_Relational_Comp
FStar_Relational_State
FStar_Seq
FStar_Seq_Permutation
FStar_Seq_Sorted
FStar_Sequence
FStar_Sequence_Ambient
FStar_Sequence_Base
FStar_Sequence_Util
FStar_Sequence_Permutation
FStar_Sequence_Seq
FStar_Squash
FStar_SquashProperties
FStar_StrongExcludedMiddle
FStar_Tcp
FStar_TwoLevelHeap
FStar_Udp
FStar_Universe_PCM
LowStar_Monotonic_Buffer
LowStar_Buffer
LowStar_BufferCompat
LowStar_BufferOps
LowStar_BufferView
LowStar_BufferView_Down
LowStar_BufferView_Up
LowStar_Comment
LowStar_ImmutableBuffer
LowStar_ConstBuffer
LowStar_Endianness
LowStar_Modifies
LowStar_ModifiesPat
LowStar_PrefixFreezableBuffer
LowStar_Regional
LowStar_Vector
LowStar_RVector
LowStar_Regional_Instances
LowStar_ToFStarBuffer
LowStar_UninitializedBuffer
Steel_Common
Steel_Effect
Steel_HigherReference
Steel_MonotonicHigherReference
Steel_Primitive_ForkJoin
Steel_Reference
Steel_SpinLock
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page