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 | (25786 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 | (996 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 | (807 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 | (1538 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 | (584 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 | (11835 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 | (956 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 | (627 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 | (306 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 | (475 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 | (493 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 | (903 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 | (1194 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 | (4910 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 | (162 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 | (25786 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 | (996 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 | (807 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 | (1538 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 | (584 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 | (11835 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 | (956 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 | (627 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 | (306 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 | (475 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 | (493 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 | (903 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 | (1194 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 | (4910 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 | (162 entries) |