Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25958 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (999 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (811 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1769 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (587 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11879 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (960 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (508 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (307 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (479 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (495 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (905 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1199 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4894 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (166 entries)

R (definition)

R [in Coq.Vectors.Fin]
R [in Coq.Logic.Berardi]
Rabs [in Coq.Reals.Rbasic_fun]
Rabst_morphism [in Coq.Reals.ClassicalConstructiveReals]
Rabs_quot [in Coq.Reals.ClassicalConstructiveReals]
radd_term [in Coq.micromega.Tauto]
Ratan_seq [in Coq.Reals.Ratan]
ratom [in Coq.micromega.Tauto]
Raw.add [in Coq.FSets.FMapAVL]
Raw.add [in Coq.FSets.FMapWeakList]
Raw.add [in Coq.FSets.FMapList]
Raw.assert_false [in Coq.FSets.FMapAVL]
Raw.at_least_one_then_f [in Coq.FSets.FMapWeakList]
Raw.at_least_one [in Coq.FSets.FMapWeakList]
Raw.at_least_right [in Coq.FSets.FMapWeakList]
Raw.at_least_left [in Coq.FSets.FMapWeakList]
Raw.at_least_one_then_f [in Coq.FSets.FMapList]
Raw.at_least_one [in Coq.FSets.FMapList]
Raw.bal [in Coq.FSets.FMapAVL]
Raw.bst_sind [in Coq.FSets.FMapAVL]
Raw.bst_ind [in Coq.FSets.FMapAVL]
Raw.cardinal [in Coq.FSets.FMapAVL]
Raw.check [in Coq.FSets.FMapWeakList]
Raw.combine [in Coq.FSets.FMapWeakList]
Raw.combine [in Coq.FSets.FMapList]
Raw.combine_r [in Coq.FSets.FMapWeakList]
Raw.combine_l [in Coq.FSets.FMapWeakList]
Raw.concat [in Coq.FSets.FMapAVL]
Raw.cons [in Coq.FSets.FMapAVL]
Raw.create [in Coq.FSets.FMapAVL]
Raw.elements [in Coq.FSets.FMapAVL]
Raw.elements [in Coq.FSets.FMapWeakList]
Raw.elements [in Coq.FSets.FMapList]
Raw.elements_aux [in Coq.FSets.FMapAVL]
Raw.empty [in Coq.FSets.FMapAVL]
Raw.Empty [in Coq.FSets.FMapWeakList]
Raw.empty [in Coq.FSets.FMapWeakList]
Raw.Empty [in Coq.FSets.FMapList]
Raw.empty [in Coq.FSets.FMapList]
Raw.enumeration_sind [in Coq.FSets.FMapAVL]
Raw.enumeration_rec [in Coq.FSets.FMapAVL]
Raw.enumeration_ind [in Coq.FSets.FMapAVL]
Raw.enumeration_rect [in Coq.FSets.FMapAVL]
Raw.equal [in Coq.FSets.FMapAVL]
Raw.equal [in Coq.FSets.FMapWeakList]
Raw.equal [in Coq.FSets.FMapList]
Raw.equal_end [in Coq.FSets.FMapAVL]
Raw.equal_cont [in Coq.FSets.FMapAVL]
Raw.equal_more [in Coq.FSets.FMapAVL]
Raw.Equivb [in Coq.FSets.FMapWeakList]
Raw.Equivb [in Coq.FSets.FMapList]
Raw.find [in Coq.FSets.FMapAVL]
Raw.find [in Coq.FSets.FMapWeakList]
Raw.find [in Coq.FSets.FMapList]
Raw.fold [in Coq.FSets.FMapAVL]
Raw.fold [in Coq.FSets.FMapWeakList]
Raw.fold [in Coq.FSets.FMapList]
Raw.fold_right_pair [in Coq.FSets.FMapWeakList]
Raw.fold_right_pair [in Coq.FSets.FMapList]
Raw.gt_tree [in Coq.FSets.FMapAVL]
Raw.height [in Coq.FSets.FMapAVL]
Raw.In_sind [in Coq.FSets.FMapAVL]
Raw.In_ind [in Coq.FSets.FMapAVL]
Raw.In0 [in Coq.FSets.FMapAVL]
Raw.is_empty [in Coq.FSets.FMapAVL]
Raw.is_empty [in Coq.FSets.FMapWeakList]
Raw.is_empty [in Coq.FSets.FMapList]
Raw.join [in Coq.FSets.FMapAVL]
Raw.key [in Coq.FSets.FMapAVL]
Raw.key [in Coq.FSets.FMapWeakList]
Raw.key [in Coq.FSets.FMapList]
Raw.lt_tree [in Coq.FSets.FMapAVL]
Raw.map [in Coq.FSets.FMapAVL]
Raw.map [in Coq.FSets.FMapWeakList]
Raw.map [in Coq.FSets.FMapList]
Raw.mapi [in Coq.FSets.FMapAVL]
Raw.mapi [in Coq.FSets.FMapWeakList]
Raw.mapi [in Coq.FSets.FMapList]
Raw.MapsTo_sind [in Coq.FSets.FMapAVL]
Raw.MapsTo_ind [in Coq.FSets.FMapAVL]
Raw.map_option [in Coq.FSets.FMapAVL]
Raw.map2 [in Coq.FSets.FMapAVL]
Raw.map2 [in Coq.FSets.FMapWeakList]
Raw.map2 [in Coq.FSets.FMapList]
Raw.map2_opt [in Coq.FSets.FMapAVL]
Raw.map2_alt [in Coq.FSets.FMapList]
Raw.map2_r [in Coq.FSets.FMapList]
Raw.map2_l [in Coq.FSets.FMapList]
Raw.mem [in Coq.FSets.FMapAVL]
Raw.mem [in Coq.FSets.FMapWeakList]
Raw.mem [in Coq.FSets.FMapList]
Raw.merge [in Coq.FSets.FMapAVL]
Raw.of_pos [in Coq.Strings.OctalString]
Raw.of_pos [in Coq.Strings.HexString]
Raw.of_pos [in Coq.Strings.BinaryString]
Raw.option_cons [in Coq.FSets.FMapWeakList]
Raw.option_cons [in Coq.FSets.FMapList]
Raw.Proofs.Empty [in Coq.FSets.FMapAVL]
Raw.Proofs.Equivb [in Coq.FSets.FMapAVL]
Raw.Proofs.flatten_e [in Coq.FSets.FMapAVL]
Raw.Proofs.fold' [in Coq.FSets.FMapAVL]
Raw.Proofs.IfEq [in Coq.FSets.FMapAVL]
Raw.remove [in Coq.FSets.FMapAVL]
Raw.remove [in Coq.FSets.FMapWeakList]
Raw.remove [in Coq.FSets.FMapList]
Raw.remove_min [in Coq.FSets.FMapAVL]
Raw.split [in Coq.FSets.FMapAVL]
Raw.Submap [in Coq.FSets.FMapWeakList]
Raw.submap [in Coq.FSets.FMapWeakList]
Raw.t [in Coq.FSets.FMapWeakList]
Raw.t [in Coq.FSets.FMapList]
Raw.to_N_of_pos [in Coq.Strings.OctalString]
Raw.to_N [in Coq.Strings.OctalString]
Raw.to_N_of_pos [in Coq.Strings.HexString]
Raw.to_N [in Coq.Strings.HexString]
Raw.to_N_of_pos [in Coq.Strings.BinaryString]
Raw.to_N [in Coq.Strings.BinaryString]
Raw.tree_sind [in Coq.FSets.FMapAVL]
Raw.tree_rec [in Coq.FSets.FMapAVL]
Raw.tree_ind [in Coq.FSets.FMapAVL]
Raw.tree_rect [in Coq.FSets.FMapAVL]
Raw2SetsOn.compare [in Coq.MSets.MSetInterface]
Raw2SetsOn.lt [in Coq.MSets.MSetInterface]
Raw2SetsOn.max_elt [in Coq.MSets.MSetInterface]
Raw2SetsOn.min_elt [in Coq.MSets.MSetInterface]
RbaseSymbolsImpl.R [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rabst [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rlt [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rlt_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rmult [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rmult_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Ropp [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Ropp_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rplus [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rplus_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rquot1 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rquot2 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rrepr [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R0 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R0_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R1 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R1_def [in Coq.Reals.Rdefinitions]
Rcompare [in Coq.Reals.ROrderedType]
Rcst_sind [in Coq.micromega.RMicromega]
Rcst_rec [in Coq.micromega.RMicromega]
Rcst_ind [in Coq.micromega.RMicromega]
Rcst_rect [in Coq.micromega.RMicromega]
rdeduce [in Coq.micromega.RMicromega]
Rdist [in Coq.Reals.Rfunctions]
Rdiv [in Coq.Reals.Rdefinitions]
rectS [in Coq.Vectors.Fin]
rectS [in Coq.Vectors.VectorDef]
rect2 [in Coq.Vectors.Fin]
rect2 [in Coq.Vectors.VectorDef]
reduce [in Coq.btauto.Algebra]
reduce_aux [in Coq.btauto.Algebra]
reflect_sind [in Coq.Bool.Bool]
reflect_rec [in Coq.Bool.Bool]
reflect_ind [in Coq.Bool.Bool]
reflect_rect [in Coq.Bool.Bool]
reflexive [in Coq.ssr.ssrbool]
Reflexive [in Coq.Sets.Relations_1]
reflexive [in Coq.Relations.Relation_Definitions]
rel [in Coq.ssr.ssrbool]
Rel [in Coq.Sets.Partial_Order]
Relation [in Coq.Sets.Relations_1]
relation [in Coq.Relations.Relation_Definitions]
RelationalChoice_on [in Coq.Logic.ChoiceFacts]
relation_disjunction [in Coq.Classes.RelationClasses]
relation_conjunction [in Coq.Classes.RelationClasses]
relation_equivalence [in Coq.Classes.RelationClasses]
relation_disjunction [in Coq.Classes.CRelationClasses]
relation_conjunction [in Coq.Classes.CRelationClasses]
relation_equivalence [in Coq.Classes.CRelationClasses]
RelCompFun [in Coq.Classes.RelationPairs]
relpre [in Coq.ssr.ssrbool]
RelProd [in Coq.Classes.RelationPairs]
relU [in Coq.ssr.ssrbool]
rel_ls_sind [in Coq.Logic.ConstructiveEpsilon]
rel_ls_ind [in Coq.Logic.ConstructiveEpsilon]
rel_of_simpl [in Coq.ssr.ssrbool]
rel_prime_dec [in Coq.ZArith.Znumtheory]
rel_prime [in Coq.ZArith.Znumtheory]
Remainder [in Coq.ZArith.Zdiv]
Remainder [in Coq.ZArith.Zquot]
Remainder_alt [in Coq.ZArith.Zdiv]
Remainder_alt [in Coq.ZArith.Zquot]
remove [in Coq.Lists.List]
removeA [in Coq.Lists.SetoidList]
removelast [in Coq.Lists.List]
remove' [in Coq.Lists.List]
repeat [in Coq.Lists.List]
replace [in Coq.Vectors.VectorDef]
replace_order [in Coq.Vectors.VectorDef]
RepresentativeFunctionalChoice_on [in Coq.Logic.ChoiceFacts]
Reqb [in Coq.Reals.ROrderedType]
Req_constr [in Coq.Reals.ClassicalConstructiveReals]
respectful [in Coq.Classes.Morphisms]
respectful [in Coq.Classes.CMorphisms]
respectful_hetero [in Coq.Classes.Morphisms]
respectful_hetero [in Coq.Classes.CMorphisms]
respecting [in Coq.Classes.CEquivalence]
respecting [in Coq.Classes.Equivalence]
Reste [in Coq.Reals.Cos_rel]
Reste_E [in Coq.Reals.Exp_prop]
Reste1 [in Coq.Reals.Cos_rel]
Reste2 [in Coq.Reals.Cos_rel]
returnType [in Coq.ssr.ssreflect]
rev [in Coq.Init.Decimal]
rev [in Coq.Lists.List]
rev [in Coq.Init.Hexadecimal]
rev [in Coq.Vectors.VectorDef]
Reval_formula' [in Coq.micromega.RMicromega]
Reval_formula [in Coq.micromega.RMicromega]
Reval_op2 [in Coq.micromega.RMicromega]
Reval_bop2 [in Coq.micromega.RMicromega]
Reval_pop2 [in Coq.micromega.RMicromega]
Reval_expr [in Coq.micromega.RMicromega]
revapp [in Coq.Init.Decimal]
revapp [in Coq.Init.Hexadecimal]
ReverseCoercionSource [in Coq.Init.Prelude]
ReverseCoercionTarget [in Coq.Init.Prelude]
reverse_coercion [in Coq.Init.Prelude]
rev_append [in Coq.Lists.List]
rev_left_loop [in Coq.ssr.ssrfun]
rev_right_loop [in Coq.ssr.ssrfun]
rev_append [in Coq.Vectors.VectorDef]
rev_append_tail [in Coq.Vectors.VectorDef]
rev' [in Coq.Lists.List]
Rfloor [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Rge [in Coq.Reals.Rdefinitions]
Rgt [in Coq.Reals.Rdefinitions]
RHasMinMax.max [in Coq.Reals.Rminmax]
RHasMinMax.max_r [in Coq.Reals.Rminmax]
RHasMinMax.max_l [in Coq.Reals.Rminmax]
RHasMinMax.min [in Coq.Reals.Rminmax]
RHasMinMax.min_r [in Coq.Reals.Rminmax]
RHasMinMax.min_l [in Coq.Reals.Rminmax]
RiemannInt [in Coq.Reals.RiemannInt]
RiemannInt_SF [in Coq.Reals.RiemannInt_SF]
Riemann_integrable [in Coq.Reals.RiemannInt]
RightDistributivityImplicationOverDisjunction [in Coq.Logic.ClassicalFacts]
right_transitive [in Coq.ssr.ssrbool]
right_distributive [in Coq.ssr.ssrfun]
right_zero [in Coq.ssr.ssrfun]
right_loop [in Coq.ssr.ssrfun]
right_commutative [in Coq.ssr.ssrfun]
right_id [in Coq.ssr.ssrfun]
right_injective [in Coq.ssr.ssrfun]
right_inverse [in Coq.ssr.ssrfun]
ring_subst_niter [in Coq.setoid_ring.Ring_tac]
ring_kind_sind [in Coq.setoid_ring.Ring_theory]
ring_kind_rec [in Coq.setoid_ring.Ring_theory]
ring_kind_ind [in Coq.setoid_ring.Ring_theory]
ring_kind_rect [in Coq.setoid_ring.Ring_theory]
RinvImpl.Rinv [in Coq.Reals.Rdefinitions]
RinvImpl.Rinv_def [in Coq.Reals.Rdefinitions]
RinvN [in Coq.Reals.RiemannInt]
Rinv_quot [in Coq.Reals.ClassicalConstructiveReals]
Rle [in Coq.Reals.Rdefinitions]
Rle [in Coq.Reals.ClassicalDedekindReals]
Rln [in Coq.Reals.Rpower]
Rlog [in Coq.Reals.Rpower]
Rlt_epsilon [in Coq.Reals.ClassicalConstructiveReals]
Rmax [in Coq.Reals.Rbasic_fun]
Rmax_N [in Coq.Reals.Rseries]
Rmin [in Coq.Reals.Rbasic_fun]
Rminus [in Coq.Reals.Rdefinitions]
Rmult_pos_pos [in Coq.Reals.RIneq]
Rmult_inv_l [in Coq.Reals.RIneq]
Rmult_inv_r [in Coq.Reals.RIneq]
Rnegate [in Coq.micromega.RMicromega]
Rnormalise [in Coq.micromega.RMicromega]
Ropp_Ropp_IZR [in Coq.Reals.RIneq]
Rops_wd [in Coq.micromega.RingMicromega]
ror_cnf_opt [in Coq.micromega.Tauto]
ror_cnf [in Coq.micromega.Tauto]
ror_clause_cnf [in Coq.micromega.Tauto]
ror_clause [in Coq.micromega.Tauto]
round_nearest_even [in Coq.Floats.SpecFloat]
Rplus_sind [in Coq.Sets.Relations_2]
Rplus_ind [in Coq.Sets.Relations_2]
Rpower [in Coq.Reals.Rpower]
Rrepr_morphism [in Coq.Reals.ClassicalConstructiveReals]
RRle_abs [in Coq.Reals.Rbasic_fun]
Rsqr [in Coq.Reals.RIneq]
Rsqrt [in Coq.Reals.Rsqrt_def]
Rsrt [in Coq.micromega.RMicromega]
Rstar_sind [in Coq.Sets.Relations_2]
Rstar_ind [in Coq.Sets.Relations_2]
Rstar1_sind [in Coq.Sets.Relations_2]
Rstar1_ind [in Coq.Sets.Relations_2]
Rtail [in Coq.Reals.RList]
RTautoChecker [in Coq.micromega.RMicromega]
Rtheory [in Coq.nsatz.NsatzTactic]
rtyp [in Coq.micromega.Tauto]
runsat [in Coq.micromega.RMicromega]
Rup_nat [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
RWeakChecker [in Coq.micromega.RMicromega]
RWitness [in Coq.micromega.RMicromega]
rxcnf [in Coq.micromega.Tauto]
rxcnf_iff [in Coq.micromega.Tauto]
rxcnf_impl [in Coq.micromega.Tauto]
rxcnf_or [in Coq.micromega.Tauto]
rxcnf_and [in Coq.micromega.Tauto]
r_list_pow [in Coq.setoid_ring.Ring_polynom]
R_wf [in Coq.ZArith.Wf_Z]
R_met [in Coq.Reals.Rlimit]
R_of_Rcst [in Coq.micromega.RMicromega]
R_as_OT.compare_spec [in Coq.Reals.ROrderedType]
R_as_OT.compare [in Coq.Reals.ROrderedType]
R_as_OT.le [in Coq.Reals.ROrderedType]
R_as_OT.lt [in Coq.Reals.ROrderedType]
R_as_UBE.eqb_eq [in Coq.Reals.ROrderedType]
R_as_UBE.eqb [in Coq.Reals.ROrderedType]
R_as_UBE.eq [in Coq.Reals.ROrderedType]
R_as_UBE.t [in Coq.Reals.ROrderedType]
R2 [in Coq.nsatz.NsatzTactic]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25958 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (999 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (811 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1769 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (587 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11879 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (960 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (508 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (307 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (479 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (495 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (905 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1199 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4894 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (166 entries)