| 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 | (26611 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 | (1022 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 | (806 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 | (1548 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 | (595 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 | (12054 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 | (959 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 | (629 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 | (308 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 | (505 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 | (912 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 | (1508 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 | (5124 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) |
B
B [definition, in Coq.Wellfounded.Well_Ordering]BackportEq [module, in Coq.Structures.Equalities]
BackportEq.eq_trans [definition, in Coq.Structures.Equalities]
BackportEq.eq_sym [definition, in Coq.Structures.Equalities]
BackportEq.eq_refl [definition, in Coq.Structures.Equalities]
Backport_OT.compare [definition, in Coq.Structures.OrdersAlt]
Backport_OT.lt_trans [lemma, in Coq.Structures.OrdersAlt]
Backport_OT.lt_not_eq [lemma, in Coq.Structures.OrdersAlt]
Backport_OT.lt [definition, in Coq.Structures.OrdersAlt]
Backport_OT [module, in Coq.Structures.OrdersAlt]
Backport_DT [module, in Coq.Structures.Equalities]
Backport_ET [module, in Coq.Structures.Equalities]
Backport_Sets.E [module, in Coq.FSets.FSetCompat]
Backport_Sets.compare [definition, in Coq.FSets.FSetCompat]
Backport_Sets.lt_not_eq [lemma, in Coq.FSets.FSetCompat]
Backport_Sets.lt_trans [definition, in Coq.FSets.FSetCompat]
Backport_Sets.choose_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.elements_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt_2 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt_1 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt_2 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt_1 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt [definition, in Coq.FSets.FSetCompat]
Backport_Sets.lt [definition, in Coq.FSets.FSetCompat]
Backport_Sets [module, in Coq.FSets.FSetCompat]
Backport_WSets.elements_3w [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elements_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elements_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.choose_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.choose_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.partition_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.partition_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.exists_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.exists_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.for_all_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.for_all_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.cardinal_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.fold_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.singleton_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.singleton_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.is_empty_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.is_empty_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.empty_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.subset_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.subset_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.equal_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.equal_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.mem_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.mem_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_trans [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_sym [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_refl [definition, in Coq.FSets.FSetCompat]
Backport_WSets.In_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.MF [module, in Coq.FSets.FSetCompat]
Backport_WSets.choose [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elements [definition, in Coq.FSets.FSetCompat]
Backport_WSets.cardinal [definition, in Coq.FSets.FSetCompat]
Backport_WSets.partition [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter [definition, in Coq.FSets.FSetCompat]
Backport_WSets.exists_ [definition, in Coq.FSets.FSetCompat]
Backport_WSets.for_all [definition, in Coq.FSets.FSetCompat]
Backport_WSets.fold [definition, in Coq.FSets.FSetCompat]
Backport_WSets.subset [definition, in Coq.FSets.FSetCompat]
Backport_WSets.equal [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_dec [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove [definition, in Coq.FSets.FSetCompat]
Backport_WSets.singleton [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add [definition, in Coq.FSets.FSetCompat]
Backport_WSets.mem [definition, in Coq.FSets.FSetCompat]
Backport_WSets.is_empty [definition, in Coq.FSets.FSetCompat]
Backport_WSets.empty [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Exists [definition, in Coq.FSets.FSetCompat]
Backport_WSets.For_all [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Empty [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Subset [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Equal [definition, in Coq.FSets.FSetCompat]
Backport_WSets.In [definition, in Coq.FSets.FSetCompat]
Backport_WSets.t [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elt [definition, in Coq.FSets.FSetCompat]
Backport_WSets [module, in Coq.FSets.FSetCompat]
Bag [constructor, in Coq.Sets.Multiset]
BalanceProps [module, in Coq.MSets.MSetRBT]
BalanceProps.add_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.append_arb_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.arbt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.arb_nr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.arb_nrr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ARB_RR [constructor, in Coq.MSets.MSetRBT]
BalanceProps.ARB_RB [constructor, in Coq.MSets.MSetRBT]
BalanceProps.Bk [abbreviation, in Coq.MSets.MSetRBT]
BalanceProps.del_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.del_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.diff_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.filter_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.fold_remove_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.fold_add_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.ifred [definition, in Coq.MSets.MSetRBT]
BalanceProps.ifred_or [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ifred_notred [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ins_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ins_rr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.inter_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.lbalS_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.lbalS_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.lbal_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.makeBlack_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.makeRed_rr [lemma, in Coq.MSets.MSetRBT]
BalanceProps.maxdepth_lowerbound [lemma, in Coq.MSets.MSetRBT]
BalanceProps.maxdepth_upperbound [lemma, in Coq.MSets.MSetRBT]
BalanceProps.partition_rb2 [instance, in Coq.MSets.MSetRBT]
BalanceProps.partition_rb1 [instance, in Coq.MSets.MSetRBT]
BalanceProps.rbalS_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rbalS_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rbal_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rbal'_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.RBT [projection, in Coq.MSets.MSetRBT]
BalanceProps.Rbt [record, in Coq.MSets.MSetRBT]
BalanceProps.RBT [constructor, in Coq.MSets.MSetRBT]
BalanceProps.Rbt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.rbt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.rbt_ind [definition, in Coq.MSets.MSetRBT]
BalanceProps.rb_mindepth [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rb_maxdepth [lemma, in Coq.MSets.MSetRBT]
BalanceProps.RB_Bk [constructor, in Coq.MSets.MSetRBT]
BalanceProps.RB_Rd [constructor, in Coq.MSets.MSetRBT]
BalanceProps.RB_Leaf [constructor, in Coq.MSets.MSetRBT]
BalanceProps.Rd [abbreviation, in Coq.MSets.MSetRBT]
BalanceProps.redcarac [definition, in Coq.MSets.MSetRBT]
BalanceProps.remove_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.rrt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.rr_nrr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.RR_Rd [constructor, in Coq.MSets.MSetRBT]
BalanceProps.singleton_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.treeify_aux_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_cont_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_one_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_zero_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_rb_invariant [definition, in Coq.MSets.MSetRBT]
BalanceProps.union_rb [lemma, in Coq.MSets.MSetRBT]
Ball_in_inter [lemma, in Coq.Reals.PSeries_reg]
barred [definition, in Coq.Logic.WeakFan]
base [definition, in Coq.Numbers.Cyclic.Abstract.DoubleType]
base [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Base [projection, in Coq.Reals.Rlimit]
BASES [section, in Coq.Vectors.VectorDef]
_ ++ _ [notation, in Coq.Vectors.VectorDef]
base_Int_part [lemma, in Coq.Reals.R_Ifp]
base_fp [lemma, in Coq.Reals.R_Ifp]
Basics [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics [library]
Basics.EqShiftL [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Incr [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Incr.Incr [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Phi [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Phi.Phi [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.A [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.caserec [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.case0 [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.case0_caserec [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Bcons [definition, in Coq.Bool.Bvector]
bdepth [definition, in Coq.micromega.ZMicromega]
Beep [definition, in Coq.Strings.Ascii]
before_witness_dep_ind [definition, in Coq.Logic.ConstructiveEpsilon]
before_witness_sind [definition, in Coq.Logic.ConstructiveEpsilon]
before_witness_ind [definition, in Coq.Logic.ConstructiveEpsilon]
before_witness [inductive, in Coq.Logic.ConstructiveEpsilon]
BEQ [section, in Coq.Vectors.VectorEq]
beq_poly [definition, in Coq.btauto.Algebra]
beq_nat_eq [abbreviation, in Coq.Arith.EqNat]
beq_nat_eq_stt [definition, in Coq.Arith.EqNat]
beq_nat_false [abbreviation, in Coq.Arith.EqNat]
beq_nat_false_stt [definition, in Coq.Arith.EqNat]
beq_nat_true [abbreviation, in Coq.Arith.EqNat]
beq_nat_true_stt [definition, in Coq.Arith.EqNat]
beq_nat_refl [abbreviation, in Coq.Arith.EqNat]
beq_nat_refl_stt [definition, in Coq.Arith.EqNat]
beq_nat_false_iff [abbreviation, in Coq.Arith.EqNat]
beq_nat_true_iff [abbreviation, in Coq.Arith.EqNat]
beq_nat [abbreviation, in Coq.Arith.EqNat]
beq_false_not_eq [definition, in Coq.Bool.BoolEq]
beq_eq_not_false [definition, in Coq.Bool.BoolEq]
beq_eq_true [definition, in Coq.Bool.BoolEq]
BEQ.A [variable, in Coq.Vectors.VectorEq]
BEQ.A_eqb_eq [variable, in Coq.Vectors.VectorEq]
BEQ.A_beq [variable, in Coq.Vectors.VectorEq]
Berardi [library]
Berardis_paradox.Retracts.B [variable, in Coq.Logic.Berardi]
Berardis_paradox.Retracts.A [variable, in Coq.Logic.Berardi]
Berardis_paradox.Retracts [section, in Coq.Logic.Berardi]
Berardis_paradox.F [variable, in Coq.Logic.Berardi]
Berardis_paradox.T [variable, in Coq.Logic.Berardi]
Berardis_paradox.Bool [variable, in Coq.Logic.Berardi]
Berardis_paradox.EM [variable, in Coq.Logic.Berardi]
Berardis_paradox [section, in Coq.Logic.Berardi]
between [inductive, in Coq.Arith.Between]
Between [section, in Coq.Arith.Between]
Between [library]
between_not_exists [lemma, in Coq.Arith.Between]
between_or_exists [lemma, in Coq.Arith.Between]
between_in_int [lemma, in Coq.Arith.Between]
between_restr [lemma, in Coq.Arith.Between]
between_Sk_l [lemma, in Coq.Arith.Between]
between_le [lemma, in Coq.Arith.Between]
between_sind [definition, in Coq.Arith.Between]
between_ind [definition, in Coq.Arith.Between]
Between.P [variable, in Coq.Arith.Between]
Between.Q [variable, in Coq.Arith.Between]
bet_eq [lemma, in Coq.Arith.Between]
bet_S [constructor, in Coq.Arith.Between]
bet_emp [constructor, in Coq.Arith.Between]
Bezout [inductive, in Coq.ZArith.Znumtheory]
bezout_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Bezout_sind [definition, in Coq.ZArith.Znumtheory]
Bezout_ind [definition, in Coq.ZArith.Znumtheory]
Bezout_intro [constructor, in Coq.ZArith.Znumtheory]
BFormula [definition, in Coq.micromega.Tauto]
bFun [definition, in Coq.Logic.FinFun]
Bhigh [definition, in Coq.Bool.Bvector]
BijComp_FunctExt [lemma, in Coq.Logic.ExtensionalityFacts]
Bijections [section, in Coq.ssr.ssrfun]
BijectionsTheory [section, in Coq.ssr.ssrfun]
BijectionsTheory.A [variable, in Coq.ssr.ssrfun]
BijectionsTheory.B [variable, in Coq.ssr.ssrfun]
BijectionsTheory.C [variable, in Coq.ssr.ssrfun]
BijectionsTheory.f [variable, in Coq.ssr.ssrfun]
BijectionsTheory.h [variable, in Coq.ssr.ssrfun]
Bijections.A [variable, in Coq.ssr.ssrfun]
Bijections.B [variable, in Coq.ssr.ssrfun]
Bijections.bijf [variable, in Coq.ssr.ssrfun]
Bijections.f [variable, in Coq.ssr.ssrfun]
Bijective [constructor, in Coq.ssr.ssrfun]
bijective [inductive, in Coq.ssr.ssrfun]
Bijective [definition, in Coq.Logic.FinFun]
bijective_on [definition, in Coq.ssr.ssrbool]
bijective_in [definition, in Coq.ssr.ssrbool]
BijectivityBijectiveComp [abbreviation, in Coq.Logic.ExtensionalityFacts]
bij_can_bij [lemma, in Coq.ssr.ssrfun]
bij_comp [lemma, in Coq.ssr.ssrfun]
bij_can_eq [lemma, in Coq.ssr.ssrfun]
bij_can_sym [lemma, in Coq.ssr.ssrfun]
bij_inj [lemma, in Coq.ssr.ssrfun]
Binary [section, in Coq.Classes.RelationClasses]
Binary [section, in Coq.Classes.CRelationClasses]
BinaryString [library]
binary_relation [definition, in Coq.Classes.RelationClasses]
binary_operation [definition, in Coq.Classes.RelationClasses]
binary_normalize [definition, in Coq.Floats.SpecFloat]
binary_round [definition, in Coq.Floats.SpecFloat]
binary_round_aux [definition, in Coq.Floats.SpecFloat]
binary_to_Z_to_binary [lemma, in Coq.ZArith.Zdigits]
binary_value_pos [lemma, in Coq.ZArith.Zdigits]
binary_value_Sn [lemma, in Coq.ZArith.Zdigits]
binary_value [lemma, in Coq.ZArith.Zdigits]
Binder [module, in Ltac2.Constr]
bind_unless [lemma, in Coq.ssr.ssrbool]
BinInt [library]
BinIntDef [library]
bInjective [definition, in Coq.Logic.FinFun]
bInjective_bSurjective [lemma, in Coq.Logic.FinFun]
BinList [library]
BinNat [library]
BinNatDef [library]
BinNums [library]
binomial [lemma, in Coq.Reals.Binomial]
Binomial [library]
BinOp [record, in Coq.micromega.ZifyClasses]
BinOpSpec [record, in Coq.micromega.ZifyClasses]
BinOp_Zcompare [instance, in Coq.micromega.ZifyComparison]
BinPos [library]
BinPosDef [library]
BinRel [record, in Coq.micromega.ZifyClasses]
Bintree [library]
bit [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
bitE [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
Bits [module, in Coq.Numbers.NatInt.NZBits]
BitsNotation [module, in Coq.Numbers.NatInt.NZBits]
_ << _ [notation, in Coq.Numbers.NatInt.NZBits]
_ >> _ [notation, in Coq.Numbers.NatInt.NZBits]
_ .[ _ ] [notation, in Coq.Numbers.NatInt.NZBits]
Bits' [module, in Coq.Numbers.NatInt.NZBits]
Bits.div2 [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.land [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.ldiff [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.lor [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.lxor [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.shiftl [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.shiftr [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.testbit [axiom, in Coq.Numbers.NatInt.NZBits]
bitwise [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
bitwise [definition, in Coq.Init.Nat]
bit_value [definition, in Coq.ZArith.Zdigits]
bit_add_or [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_0 [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_lsl [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_ext [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_half [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_M [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_1 [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_b2i [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_lsr [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_split [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
bit_0_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
Black [constructor, in Coq.MSets.MSetRBT]
block [definition, in Coq.Program.Equality]
Blow [definition, in Coq.Bool.Bvector]
Bneg [definition, in Coq.Bool.Bvector]
Bnil [definition, in Coq.Bool.Bvector]
Bnth [abbreviation, in Coq.NArith.Ndigits]
Bnth_Nbit [lemma, in Coq.NArith.Ndigits]
Bolzano_Weierstrass [lemma, in Coq.Reals.Rtopology]
Bool [section, in Coq.Lists.List]
bool [inductive, in Coq.Init.Datatypes]
Bool [section, in Coq.btauto.Reflect]
Bool [library]
Bool [library]
BooleanDecidableType [module, in Coq.Structures.Equalities]
BooleanDecidableType' [module, in Coq.Structures.Equalities]
BooleanEqualityType [module, in Coq.Structures.Equalities]
BooleanEqualityType' [module, in Coq.Structures.Equalities]
BOOLEAN_VECTORS [section, in Coq.Bool.Bvector]
boolean_witness_nonzero [lemma, in Coq.btauto.Reflect]
boolean_witness [definition, in Coq.btauto.Reflect]
BoolEq [library]
BoolEqualityFacts [module, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_sym [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_refl [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_neq [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_spec [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_compat [instance, in Coq.Structures.Equalities]
boolfunPredType [definition, in Coq.ssr.ssrbool]
BoolIf [section, in Coq.ssr.ssrbool]
BoolIf.A [variable, in Coq.ssr.ssrbool]
BoolIf.b [variable, in Coq.ssr.ssrbool]
BoolIf.B [variable, in Coq.ssr.ssrbool]
BoolIf.f [variable, in Coq.ssr.ssrbool]
BoolIf.vF [variable, in Coq.ssr.ssrbool]
BoolIf.vT [variable, in Coq.ssr.ssrbool]
BoolIf.x [variable, in Coq.ssr.ssrbool]
BoolNotations [module, in Coq.Bool.Bool]
BoolNotations [module, in Ltac2.Bool]
_ =? _ (bool_scope) [notation, in Coq.Bool.Bool]
_ ?= _ (bool_scope) [notation, in Coq.Bool.Bool]
_ < _ (bool_scope) [notation, in Coq.Bool.Bool]
_ <= _ (bool_scope) [notation, in Coq.Bool.Bool]
BoolOrd [module, in Coq.Bool.BoolOrder]
BoolOrder [library]
BoolOrderFacts [module, in Coq.Structures.OrdersFacts]
BoolOrderFacts.eqb_compare [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_compare [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_antisym [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_refl [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_gt [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_nle [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_spec [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_spec0 [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_compare [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_antisym [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_irrefl [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_ge [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_nlt [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_spec [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_spec0 [lemma, in Coq.Structures.OrdersFacts]
BoolOrdSpecs [module, in Coq.Structures.Orders]
BoolOrd.compare [definition, in Coq.Bool.BoolOrder]
BoolOrd.compare_spec [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq [definition, in Coq.Bool.BoolOrder]
BoolOrd.eqb [definition, in Coq.Bool.BoolOrder]
BoolOrd.eqb_eq [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_trans [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_sym [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_refl [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_dec [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_equiv [definition, in Coq.Bool.BoolOrder]
BoolOrd.le [definition, in Coq.Bool.BoolOrder]
BoolOrd.le_lteq [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt_total [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt_compat [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt_strorder [definition, in Coq.Bool.BoolOrder]
BoolOrd.t [definition, in Coq.Bool.BoolOrder]
boolP [lemma, in Coq.ssr.ssrbool]
boolP [inductive, in Coq.Logic.ClassicalFacts]
BoolP [definition, in Coq.Logic.ClassicalFacts]
boolP_indd [definition, in Coq.Logic.ClassicalFacts]
boolP_elim_redr [definition, in Coq.Logic.ClassicalFacts]
boolP_elim_redl [definition, in Coq.Logic.ClassicalFacts]
boolP_sind [definition, in Coq.Logic.ClassicalFacts]
boolP_ind [definition, in Coq.Logic.ClassicalFacts]
BoolP_dep_induction [definition, in Coq.Logic.ClassicalFacts]
BoolP_elim_redr [definition, in Coq.Logic.ClassicalFacts]
BoolP_elim_redl [definition, in Coq.Logic.ClassicalFacts]
BoolP_elim [definition, in Coq.Logic.ClassicalFacts]
BoolSpec [inductive, in Coq.Init.Datatypes]
BoolSpecF [constructor, in Coq.Init.Datatypes]
BoolSpecT [constructor, in Coq.Init.Datatypes]
BoolSpec_sind [definition, in Coq.Init.Datatypes]
BoolSpec_ind [definition, in Coq.Init.Datatypes]
BoolTheory [lemma, in Coq.setoid_ring.Ring]
bool_eq_ok [lemma, in Coq.setoid_ring.Ring]
bool_eq [definition, in Coq.setoid_ring.Ring]
Bool_as_DT [module, in Coq.Structures.OrdersEx]
Bool_as_OT [module, in Coq.Structures.OrdersEx]
bool_choice [lemma, in Coq.Init.Specif]
bool_6 [abbreviation, in Coq.Bool.Bool]
bool_3 [abbreviation, in Coq.Bool.Bool]
bool_1 [abbreviation, in Coq.Bool.Bool]
bool_dec [lemma, in Coq.Bool.Bool]
bool_function_eqdec [instance, in Coq.Classes.EquivDec]
bool_eqdec [instance, in Coq.Classes.EquivDec]
Bool_eq_dec.beq_eq [variable, in Coq.Bool.BoolEq]
Bool_eq_dec.beq_refl [variable, in Coq.Bool.BoolEq]
Bool_eq_dec.beq [variable, in Coq.Bool.BoolEq]
Bool_eq_dec.A [variable, in Coq.Bool.BoolEq]
Bool_eq_dec [section, in Coq.Bool.BoolEq]
bool_function_eqdec [instance, in Coq.Classes.SetoidDec]
bool_eqdec [instance, in Coq.Classes.SetoidDec]
bool_sind [definition, in Coq.Init.Datatypes]
bool_rec [definition, in Coq.Init.Datatypes]
bool_ind [definition, in Coq.Init.Datatypes]
bool_rect [definition, in Coq.Init.Datatypes]
bool_of_sumbool [definition, in Coq.Bool.Sumbool]
bool_eq_ind [definition, in Coq.Bool.Sumbool]
bool_eq_rec [definition, in Coq.Bool.Sumbool]
Bool_nat [library]
Bool.A [variable, in Coq.Lists.List]
Bool.f [variable, in Coq.Lists.List]
Bool2Dec [module, in Coq.Structures.Equalities]
Bot [constructor, in Coq.rtauto.Rtauto]
Bottom [inductive, in Coq.Sets.Cpo]
Bottom_sind [definition, in Coq.Sets.Cpo]
Bottom_rec [definition, in Coq.Sets.Cpo]
Bottom_ind [definition, in Coq.Sets.Cpo]
Bottom_rect [definition, in Coq.Sets.Cpo]
Bottom_definition [constructor, in Coq.Sets.Cpo]
Boule [definition, in Coq.Reals.PSeries_reg]
Boule_center [lemma, in Coq.Reals.PSeries_reg]
boule_in_interval [definition, in Coq.Reals.PSeries_reg]
boule_of_interval [definition, in Coq.Reals.PSeries_reg]
Boule_convex [lemma, in Coq.Reals.PSeries_reg]
Boule_lt [lemma, in Coq.Reals.Ratan]
Boule_half_to_interval [lemma, in Coq.Reals.Ratan]
bound [definition, in Coq.Reals.Raxioms]
bound [projection, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
bounded [definition, in Coq.Floats.SpecFloat]
bounded [definition, in Coq.Reals.Rtopology]
Bounds [section, in Coq.Sets.Cpo]
Bounds.C [variable, in Coq.Sets.Cpo]
Bounds.D [variable, in Coq.Sets.Cpo]
Bounds.R [variable, in Coq.Sets.Cpo]
Bounds.U [variable, in Coq.Sets.Cpo]
bound_var [definition, in Coq.micromega.ZMicromega]
Box [record, in Coq.Logic.StrictProp]
BPred [projection, in Coq.micromega.ZifyClasses]
bracket [projection, in Coq.setoid_ring.Algebra_syntax]
Bracket [record, in Coq.setoid_ring.Algebra_syntax]
bracket [constructor, in Coq.setoid_ring.Algebra_syntax]
Bracket [inductive, in Coq.setoid_ring.Algebra_syntax]
Branch [constructor, in Coq.micromega.VarMap]
Branch0 [constructor, in Coq.rtauto.Bintree]
Branch1 [constructor, in Coq.rtauto.Bintree]
BshiftL [definition, in Coq.Bool.Bvector]
BshiftL_iter [definition, in Coq.Bool.Bvector]
BshiftRa [definition, in Coq.Bool.Bvector]
BshiftRa_iter [definition, in Coq.Bool.Bvector]
BshiftRl [definition, in Coq.Bool.Bvector]
BshiftRl_iter [definition, in Coq.Bool.Bvector]
Bsign [definition, in Coq.Bool.Bvector]
BSpec [projection, in Coq.micromega.ZifyClasses]
bSurjective [definition, in Coq.Logic.FinFun]
bSurjective_bBijective [lemma, in Coq.Logic.FinFun]
Btauto [library]
Build_Setoid_Theory [definition, in Coq.Setoids.Setoid]
build_heap_sind [definition, in Coq.Sorting.Heap]
build_heap_rec [definition, in Coq.Sorting.Heap]
build_heap_ind [definition, in Coq.Sorting.Heap]
build_heap_rect [definition, in Coq.Sorting.Heap]
build_heap [inductive, in Coq.Sorting.Heap]
BVand [definition, in Coq.Bool.Bvector]
Bvector [definition, in Coq.Bool.Bvector]
Bvector [library]
BvectorNotations [module, in Coq.Bool.Bvector]
_ =? _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
_ ^| _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
_ ^⊕ _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
_ ^& _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
^~ _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
Bvect_false [definition, in Coq.Bool.Bvector]
Bvect_true [definition, in Coq.Bool.Bvector]
BVeq [definition, in Coq.Bool.Bvector]
BVor [definition, in Coq.Bool.Bvector]
BVxor [definition, in Coq.Bool.Bvector]
Bv2N [definition, in Coq.NArith.Ndigits]
Bv2N_upper_bound [lemma, in Coq.NArith.Ndigits]
Bv2N_Nsize_1 [lemma, in Coq.NArith.Ndigits]
Bv2N_Nsize [lemma, in Coq.NArith.Ndigits]
Bv2N_N2Bv [lemma, in Coq.NArith.Ndigits]
byte [inductive, in Coq.Init.Byte]
Byte [library]
Byte [library]
ByteNil [definition, in Coq.Strings.ByteVector]
ByteNotations [module, in Coq.Strings.Byte]
_ =? _ (byte_scope) [notation, in Coq.Strings.Byte]
ByteSyntaxNotations [module, in Coq.Init.Byte]
ByteVector [definition, in Coq.Strings.ByteVector]
ByteVector [library]
ByteV2N [definition, in Coq.NArith.Ndigits]
ByteV2N_upper_bound [lemma, in Coq.NArith.Ndigits]
byte_of_byte [definition, in Coq.Init.Byte]
byte_sind [definition, in Coq.Init.Byte]
byte_rec [definition, in Coq.Init.Byte]
byte_ind [definition, in Coq.Init.Byte]
byte_rect [definition, in Coq.Init.Byte]
byte_of_ascii_via_nat [lemma, in Coq.Strings.Ascii]
byte_of_ascii_via_N [lemma, in Coq.Strings.Ascii]
byte_of_ascii_of_byte [lemma, in Coq.Strings.Ascii]
byte_of_ascii [definition, in Coq.Strings.Ascii]
byte_eq_dec [definition, in Coq.Strings.Byte]
byte_dec_bl [lemma, in Coq.Strings.Byte]
byte_dec_lb [lemma, in Coq.Strings.Byte]
B1 [definition, in Coq.Reals.Cos_rel]
B1_cvg [lemma, in Coq.Reals.Cos_rel]
b2i [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
b2n_b2z [lemma, in Coq.micromega.ZifyBool]
b2zSpec [instance, in Coq.micromega.ZifyBool]
b2z_spec [lemma, in Coq.micromega.ZifyBool]
| 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 | (26611 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 | (1022 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 | (806 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 | (1548 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 | (595 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 | (12054 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 | (959 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 | (629 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 | (308 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 | (505 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 | (912 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 | (1508 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 | (5124 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) |