Rocq Standard Library: Internal Component Dependencies

Subcomponent unicode

contains

• Unicode.Utf8_core
• Unicode.Utf8

Subcomponent corelib_wrapper

contains

• Array.ArrayAxioms
• Array.PrimArray
• BinNums.IntDef
• BinNums.NatDef
• BinNums.PosDef
• Classes.CMorphisms
• Classes.CRelationClasses
• Classes.Equivalence
• Classes.Init
• Classes.Morphisms
• Classes.Morphisms_Prop
• Classes.RelationClasses
• Classes.SetoidTactics
• Compat.Coq818
• Compat.Coq819
• Compat.Coq820
• Floats.FloatAxioms
• Floats.FloatClass
• Floats.FloatOps
• Floats.PrimFloat
• Floats.SpecFloat
• Init.Byte
• Init.Datatypes
• Init.Decimal
• Init.Hexadecimal
• Init.Logic
• Init.Ltac
• Init.Nat
• Init.Notations
• Init.Number
• Init.Peano
• Init.Prelude
• Init.Specif
• Init.Sumbool
• Init.Tactics
• Init.Tauto
• Init.Wf
• Lists.ListDef
• Numbers.BinNums
• Numbers.Cyclic.Int63.CarryType
• Numbers.Cyclic.Int63.PrimInt63
• Numbers.Cyclic.Int63.Sint63Axioms
• Numbers.Cyclic.Int63.Uint63Axioms
• Program.Basics
• Program.Tactics
• Program.Utils
• Program.Wf
• Relations.Relation_Definitions
• Setoids.Setoid
• Strings.PrimString
• Strings.PrimStringAxioms
• derive.Derive
• extraction.ExtrHaskellBasic
• extraction.ExtrOcamlBasic
• extraction.Extraction
• ssr.ssrbool
• ssr.ssrclasses
• ssr.ssreflect
• ssr.ssrfun
• ssr.ssrsetoid
• ssr.ssrunder
• ssrmatching.ssrmatching

Subcomponent logic

contains

• Logic.Adjointification
• Logic.Berardi
• Logic.ConstructiveEpsilon
• Logic.Decidable
• Logic.EqdepFacts
• Logic.Eqdep
• Logic.Eqdep_dec
• Logic.ExtensionalFunctionRepresentative
• Logic.ExtensionalityFacts
• Logic.FunctionalExtensionality
• Logic.HLevelsBase
• Logic.HLevels
• Logic.Hurkens
• Logic.JMeq
• Logic.ProofIrrelevanceFacts
• Logic.ProofIrrelevance
• Logic.PropExtensionalityFacts
• Logic.PropFacts
• Logic.RelationalChoice
• Logic.SetIsType
• Logic.StrictProp
• Logic.WeakFan

Subcomponent program

depends on

• logic
• corelib_wrapper

and contains

• Program.Combinators
• Program.Equality
• Program.Subset
• Program.Syntax
• Program.WfExtensionality
• Program.Program

Subcomponent relations

depends on

• corelib_wrapper

and contains

• Relations.Relation_Operators
• Relations.Operators_Properties
• Relations.Relations

Subcomponent classes

depends on

• relations
• program

and contains

• Classes.CEquivalence
• Classes.DecidableClass
• Classes.Morphisms_Relations
• Classes.RelationPairs
• Classes.SetoidClass

Subcomponent bool

depends on

• classes

and contains

• Bool.Bool
• Bool.BoolEq
• Bool.DecBool
• Bool.IfProp

Subcomponent structures

depends on

• bool

and contains

• Structures.Equalities
• Structures.Orders
• Structures.OrdersTac
• Structures.OrdersFacts
• Structures.GenericMinMax

Subcomponent arith_base

depends on

• structures

and contains

• Numbers.NumPrelude
• Numbers.NatInt.NZAxioms
• Numbers.NatInt.NZBase
• Numbers.NatInt.NZAdd
• Numbers.NatInt.NZMul
• Numbers.NatInt.NZOrder
• Numbers.NatInt.NZAddOrder
• Numbers.NatInt.NZMulOrder
• Numbers.NatInt.NZDiv
• Numbers.NatInt.NZPow
• Numbers.NatInt.NZLog
• Numbers.NatInt.NZParity
• Numbers.NatInt.NZBits
• Numbers.NatInt.NZGcd
• Numbers.NatInt.NZSqrt
• Numbers.Natural.Abstract.NAxioms
• Numbers.Natural.Abstract.NBase
• Numbers.Natural.Abstract.NAdd
• Numbers.Natural.Abstract.NOrder
• Numbers.Natural.Abstract.NAddOrder
• Numbers.Natural.Abstract.NMulOrder
• Numbers.Natural.Abstract.NSub
• Numbers.Natural.Abstract.NDiv
• Numbers.Natural.Abstract.NParity
• Numbers.Natural.Abstract.NPow
• Numbers.Natural.Abstract.NLog
• Numbers.Natural.Abstract.NBits
• Numbers.Natural.Abstract.NDiv0
• Numbers.Natural.Abstract.NGcd
• Numbers.Natural.Abstract.NLcm
• Numbers.Natural.Abstract.NLcm0
• Numbers.Natural.Abstract.NMaxMin
• Numbers.Natural.Abstract.NSqrt
• Numbers.Natural.Abstract.NProperties
• Arith.PeanoNat
• Arith.Between
• Arith.Compare_dec
• Arith.EqNat
• Arith.Factorial
• Arith.Peano_dec
• Arith.Wf_nat
• Arith.Arith_base
• Arith.Bool_nat
• Arith.Cantor
• Arith.Compare
• Arith.Euclid
• Arith.Zerob
• Classes.SetoidDec
• Numbers.NatInt.NZDomain
• Numbers.NatInt.NZProperties
• Numbers.Natural.Abstract.NStrongRec
• Numbers.Natural.Abstract.NDefOps
• Numbers.Natural.Abstract.NIso

Subcomponent lists

depends on

• arith_base

and contains

• Lists.List
• Classes.EquivDec
• Lists.ListDec
• Lists.Finite
• Lists.ListSet
• Lists.ListTactics
• Logic.WKL
• Numbers.NaryFunctions
• Sorting.Permutation

Subcomponent positive

depends on

• arith_base

and contains

• Numbers.AltBinNotations
• PArith.BinPosDef
• PArith.BinPos
• PArith.POrderedType
• PArith.Pnat
• PArith.PArith

Subcomponent narith_base

depends on

• positive

and contains

• NArith.BinNatDef
• NArith.BinNat
• NArith.Ndiv_def
• NArith.Ngcd_def
• NArith.Nnat
• NArith.Nsqrt_def
• NArith.NArith_base
• NArith.Ndec

Subcomponent zarith_base

depends on

• narith_base

and contains

• Numbers.Integer.Abstract.ZAxioms
• Numbers.Integer.Abstract.ZBase
• Numbers.Integer.Abstract.ZAdd
• Numbers.Integer.Abstract.ZMul
• Numbers.Integer.Abstract.ZLt
• Numbers.Integer.Abstract.ZAddOrder
• Numbers.Integer.Abstract.ZMulOrder
• Numbers.Integer.Abstract.ZSgnAbs
• Numbers.Integer.Abstract.ZDivFloor
• Numbers.Integer.Abstract.ZParity
• Numbers.Integer.Abstract.ZPow
• Numbers.Integer.Abstract.ZBits
• Numbers.Integer.Abstract.ZDivEucl
• Numbers.Integer.Abstract.ZDivTrunc
• Numbers.Integer.Abstract.ZGcd
• Numbers.Integer.Abstract.ZLcm
• Numbers.Integer.Abstract.ZMaxMin
• Numbers.Integer.Abstract.ZProperties
• ZArith.BinIntDef
• ZArith.BinInt
• ZArith.Int
• ZArith.Zcompare
• ZArith.Zorder
• ZArith.Zmisc
• ZArith.Znat
• ZArith.Wf_Z
• ZArith.ZArith_dec
• ZArith.Zabs
• ZArith.Zeven
• ZArith.Zbool
• ZArith.Zmin
• ZArith.auxiliary
• ZArith.Zhints
• ZArith.Zmax
• ZArith.Zminmax
• ZArith.ZArith_base
• ZArith.Zeuclid
• ZArith.Zpow_alt

Subcomponent ring

depends on

• zarith_base
• lists

and contains

• setoid_ring.Ring_theory
• ZArith.Zpow_def
• setoid_ring.BinList
• setoid_ring.Ring_polynom
• setoid_ring.InitialRing
• setoid_ring.Ring_tac
• setoid_ring.Ring_base
• setoid_ring.Ring
• setoid_ring.ZArithRing
• ZArith.Zcomplements
• ZArith.Zdiv
• setoid_ring.Algebra_syntax
• setoid_ring.Ncring
• setoid_ring.Ncring_polynom
• setoid_ring.Ncring_initial
• setoid_ring.Ncring_tac
• setoid_ring.Cring
• setoid_ring.Integral_domain
• nsatz.NsatzTactic
• setoid_ring.ArithRing
• setoid_ring.NArithRing
• setoid_ring.Rings_Z

Subcomponent arith

depends on

• ring

and contains

• Arith.Arith

Subcomponent narith

depends on

• ring

and contains

• NArith.NArith

Subcomponent lia

depends on

• narith
• arith

and contains

• micromega.DeclConstantZ
• micromega.Env
• micromega.EnvRing
• micromega.OrderedRing
• micromega.Refl
• micromega.Tauto
• micromega.RingMicromega
• micromega.VarMap
• micromega.ZCoeff
• micromega.ZMicromega
• micromega.ZifyClasses
• micromega.ZifyInst
• micromega.Zify
• omega.PreOmega
• micromega.Lia
• micromega.ZArith_hints
• micromega.ZifyBool
• micromega.ZifyComparison
• micromega.ZifyN
• micromega.ZifyNat
• micromega.ZifyPow
• micromega.Ztac
• omega.OmegaLemmas

Subcomponent zarith

depends on

• lia

and contains

• ZArith.Zdiv_facts
• ZArith.ZModOffset
• ZArith.ZNsatz
• btauto.Algebra
• btauto.Reflect
• btauto.Btauto
• ZArith.Zbitwise
• ZArith.Zdivisibility
• ZArith.Zcong
• ZArith.Znumtheory
• ZArith.Zpower
• ZArith.ZArith
• Numbers.DecimalFacts
• Numbers.DecimalNat
• Numbers.HexadecimalFacts
• Numbers.HexadecimalNat
• Numbers.Integer.Binary.ZBinary
• Numbers.Integer.NatPairs.ZNatPairs
• Numbers.Natural.Binary.NBinary
• ZArith.Zquot
• ZArith.Zwf

Subcomponent primitive_int

depends on

• zarith
• unicode

and contains

• Numbers.Cyclic.Abstract.DoubleType
• ZArith.Zpow_facts
• Numbers.Cyclic.Abstract.CyclicAxioms
• Numbers.Cyclic.Abstract.NZCyclic
• ZArith.Zgcd_alt
• Numbers.Cyclic.Int63.Uint63
• Numbers.Cyclic.Int63.Cyclic63
• Numbers.Cyclic.Int63.Ring63
• Numbers.Cyclic.Int63.Sint63
• micromega.ZifySint63
• micromega.ZifyUint63

Subcomponent primitive_array

depends on

• primitive_int

and contains

• Array.PArray

Subcomponent primitive_floats

depends on

• primitive_int

and contains

• Floats.FloatLemmas
• Floats.Floats

Subcomponent classical_logic

depends on

• arith

and contains

• Logic.ClassicalFacts
• Logic.ChoiceFacts
• Logic.Classical_Prop
• Logic.Classical_Pred_Type
• Logic.Classical
• Logic.ClassicalUniqueChoice
• Logic.ClassicalChoice
• Logic.Description
• Logic.ClassicalDescription
• Logic.ClassicalEpsilon
• Logic.Diaconescu
• Logic.Epsilon
• Logic.IndefiniteDescription
• Logic.PropExtensionality
• Logic.SetoidChoice

Subcomponent sets

depends on

• classical_logic

and contains

• Sets.Ensembles
• Sets.Constructive_sets
• Sets.Classical_sets
• Sets.Relations_1
• Sets.Partial_Order
• Sets.Cpo
• Sets.Finite_sets
• Sets.Relations_1_facts
• Sets.Powerset
• Sets.Powerset_facts
• Sets.Powerset_Classical_facts
• Sets.Finite_sets_facts
• Sets.Image
• Sets.Infinite_sets
• Sets.Integers
• Sets.Permut
• Sets.Multiset
• Sets.Relations_2
• Sets.Relations_2_facts
• Sets.Relations_3
• Sets.Relations_3_facts
• Sets.Uniset

Subcomponent sorting

depends on

• sets
• lia

and contains

• Sorting.CPermutation
• Sorting.Sorted
• Sorting.SetoidList
• Sorting.PermutSetoid
• Sorting.Mergesort
• Sorting.Sorting
• Sorting.Heap
• Sorting.PermutEq
• Sorting.SetoidPermutation

Subcomponent strings

depends on

• arith

and contains

• Strings.Byte
• Strings.Ascii
• Strings.String
• Numbers.DecimalString
• Numbers.HexadecimalString
• Strings.BinaryString
• Strings.HexString
• Strings.OctalString

Subcomponent orders_ex

depends on

• strings
• sorting

and contains

• Structures.BoolOrder
• Structures.DecidableType
• Structures.OrderedType
• Structures.OrderedTypeEx
• Structures.DecidableTypeEx
• Structures.EqualitiesFacts
• Structures.OrderedTypeAlt
• Structures.OrdersAlt
• Structures.OrdersEx
• Structures.OrdersLists

Subcomponent primitive_string

depends on

• orders_ex
• primitive_int

and contains

• Strings.PString

Subcomponent extraction

depends on

• primitive_string
• primitive_floats
• primitive_array

and contains

• extraction.ExtrHaskellNatNum
• extraction.ExtrHaskellNatInt
• extraction.ExtrHaskellNatInteger
• extraction.ExtrHaskellString
• extraction.ExtrHaskellZNum
• extraction.ExtrHaskellZInt
• extraction.ExtrHaskellZInteger
• extraction.ExtrOCamlFloats
• extraction.ExtrOCamlInt63
• extraction.ExtrOCamlPArray
• extraction.ExtrOCamlPString
• extraction.ExtrOcamlChar
• extraction.ExtrOcamlIntConv
• extraction.ExtrOcamlNatBigInt
• extraction.ExtrOcamlNatInt
• extraction.ExtrOcamlNativeString
• extraction.ExtrOcamlString
• extraction.ExtrOcamlZBigInt
• extraction.ExtrOcamlZInt

Subcomponent fmaps_fsets_msets

depends on

• orders_ex
• zarith

and contains

• FSets.FMapInterface
• FSets.FMapList
• FSets.FMapAVL
• FSets.FMapFacts
• FSets.FMapFullAVL
• FSets.FMapPositive
• FSets.FMapWeakList
• FSets.FMaps
• FSets.FSetInterface
• FSets.FSetFacts
• MSets.MSetInterface
• MSets.MSetFacts
• FSets.FSetCompat
• MSets.MSetGenTree
• MSets.MSetAVL
• FSets.FSetAVL
• FSets.FSetBridge
• FSets.FSetDecide
• FSets.FSetProperties
• FSets.FSetEqProperties
• MSets.MSetList
• FSets.FSetList
• FSets.FSetPositive
• FSets.FSetToFiniteSet
• MSets.MSetWeakList
• FSets.FSetWeakList
• FSets.FSets
• MSets.MSetDecide
• MSets.MSetProperties
• MSets.MSetEqProperties
• MSets.MSetPositive
• MSets.MSetRBT
• MSets.MSetToFiniteSet
• MSets.MSets

Subcomponent funind

depends on

• arith_base

and contains

• funind.FunInd
• funind.Recdef

Subcomponent field

depends on

• zarith

and contains

• setoid_ring.Field_theory
• setoid_ring.Field_tac
• setoid_ring.Field

Subcomponent qarith_base

depends on

• ring

and contains

• QArith.QArith_base
• QArith.QOrderedType
• QArith.Qminmax
• QArith.Qreduction

Subcomponent lqa

depends on

• qarith_base
• field

and contains

• QArith.Qfield
• QArith.Qring
• micromega.DeclConstant
• micromega.QMicromega
• micromega.Lqa
• setoid_ring.Rings_Q

Subcomponent qarith

depends on

• lqa

and contains

• Numbers.DecimalPos
• Numbers.DecimalN
• Numbers.DecimalZ
• QArith.QNsatz
• QArith.QArith
• Numbers.DecimalQ
• Numbers.HexadecimalPos
• Numbers.HexadecimalN
• Numbers.HexadecimalZ
• Numbers.HexadecimalQ
• QArith.Qabs
• QArith.Qcanon
• QArith.Qcabs
• QArith.Qpower
• QArith.Qround

Subcomponent vectors

depends on

• lists

and contains

• Vectors.Fin
• Vectors.VectorDef
• Vectors.VectorSpec
• Vectors.VectorEq
• Vectors.Vector
• Vectors.Bvector
• Vectors.FinFun

Subcomponent reals

depends on

• vectors
• qarith
• classical_logic

and contains

• Reals.Cauchy.ConstructiveExtra
• Reals.Cauchy.PosExtra
• Reals.Cauchy.QExtra
• Reals.Cauchy.ConstructiveCauchyReals
• Reals.Cauchy.ConstructiveCauchyRealsMult
• Reals.Abstract.ConstructiveReals
• Reals.Cauchy.ConstructiveCauchyAbs
• Reals.Cauchy.ConstructiveRcomplete
• Reals.ClassicalDedekindReals
• Reals.Rdefinitions
• Numbers.DecimalR
• Numbers.HexadecimalR
• Reals.Abstract.ConstructiveAbs
• Reals.Abstract.ConstructiveLimits
• Reals.Abstract.ConstructiveRealsMorphisms
• Reals.Abstract.ConstructiveMinMax
• Reals.Abstract.ConstructiveSum
• Reals.Abstract.ConstructivePower
• Reals.Abstract.ConstructiveLUB
• Reals.Raxioms
• Reals.ClassicalConstructiveReals
• Reals.Rpow_def
• setoid_ring.RealField
• Reals.RIneq
• Reals.DiscrR
• Reals.Rbase
• Reals.R_Ifp
• Reals.Rbasic_fun
• Reals.ArithProp
• Reals.R_sqr
• Reals.SplitAbsolu
• Reals.SplitRmult
• Reals.Rfunctions
• Reals.Rseries
• Reals.SeqProp
• Reals.Rcomplete
• Reals.PartSum
• Reals.Rregisternames
• Reals.Qreals
• micromega.RMicromega
• micromega.Lra
• Reals.AltSeries
• Reals.Rlimit
• Reals.Rderiv
• Reals.Ranalysis1
• Reals.RList
• Reals.Rtopology
• Reals.MVT
• Reals.Alembert
• Reals.Binomial
• Reals.Cauchy_prod
• Reals.Rprod
• Reals.Rsigma
• Reals.SeqSeries
• Reals.PSeries_reg
• Reals.Rtrigo_fun
• Reals.Rtrigo_def
• Reals.Cos_rel
• Reals.Cos_plus
• Reals.Rsqrt_def
• Reals.Rtrigo_alt
• Reals.Rtrigo1
• Reals.Exp_prop
• Reals.R_sqrt
• Reals.Ranalysis2
• Reals.Ranalysis3
• Reals.Ranalysis4
• Reals.Rgeom
• Reals.Sqrt_reg
• Reals.Rpower
• Reals.Rtrigo_calc
• Reals.Rtrigo_reg
• Reals.Ranalysis_reg
• Reals.RiemannInt_SF
• Reals.RiemannInt
• Reals.Ranalysis5
• Reals.Rtrigo_facts
• Reals.Ratan
• Reals.Machin
• Reals.RNsatz
• Reals.Nsatz
• Reals.Rtrigo
• Reals.Ranalysis
• Reals.NewtonInt
• Reals.Integration
• Reals.Zfloor
• micromega.Fourier_util
• micromega.Fourier
• Reals.Reals
• Reals.Rlogic
• Reals.ROrderedType
• Reals.Rminmax
• Reals.Runcountable
• micromega.Psatz
• setoid_ring.Rings_R

Subcomponent rtauto

depends on

• positive
• lists

and contains

• rtauto.Bintree
• rtauto.Rtauto

Subcomponent streams

depends on

• logic

and contains

• Streams.Streams
• Streams.StreamMemo

Subcomponent wellfounded

depends on

• lists

and contains

• Wellfounded.Disjoint_Union
• Wellfounded.Inclusion
• Wellfounded.Inverse_Image
• Wellfounded.List_Extension
• Wellfounded.Transitive_Closure
• Wellfounded.Lexicographic_Exponentiation
• Wellfounded.Lexicographic_Product
• Wellfounded.Union
• Wellfounded.Well_Ordering
• Wellfounded.Wellfounded

Subcomponent zmod

depends on

• field
• sorting

and contains

• Zmod.ZmodDef
• Zmod.ZmodBase
• Zmod.Bits
• Zmod.ZstarDef
• Zmod.ZstarBase
• Zmod.ZmodInv
• Zmod.ZmodNsatz
• Zmod.Zmod
• Zmod.Zstar

Subcomponent compat

depends on

• zmod
• wellfounded
• streams
• rtauto
• reals
• funind
• fmaps_fsets_msets
• extraction

and contains

• Compat.AdmitAxiom
• Compat.Stdlib818

Subcomponent all

depends on

• compat

and contains

• All