| 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 | (26071 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 | (1003 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 | (815 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 | (1771 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 | (589 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 | (961 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 | (12021 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 | (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 | (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 | (496 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 | (906 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 | (1204 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 | (4844 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 (definition)
B [in Stdlib.Wellfounded.Well_Ordering]BackportEq.eq_trans [in Stdlib.Structures.Equalities]
BackportEq.eq_sym [in Stdlib.Structures.Equalities]
BackportEq.eq_refl [in Stdlib.Structures.Equalities]
Backport_OT.compare [in Stdlib.Structures.OrdersAlt]
Backport_OT.lt [in Stdlib.Structures.OrdersAlt]
Backport_Sets.compare [in Stdlib.FSets.FSetCompat]
Backport_Sets.lt_trans [in Stdlib.FSets.FSetCompat]
Backport_Sets.choose_3 [in Stdlib.FSets.FSetCompat]
Backport_Sets.elements_3 [in Stdlib.FSets.FSetCompat]
Backport_Sets.max_elt_3 [in Stdlib.FSets.FSetCompat]
Backport_Sets.max_elt_2 [in Stdlib.FSets.FSetCompat]
Backport_Sets.max_elt_1 [in Stdlib.FSets.FSetCompat]
Backport_Sets.min_elt_3 [in Stdlib.FSets.FSetCompat]
Backport_Sets.min_elt_2 [in Stdlib.FSets.FSetCompat]
Backport_Sets.min_elt_1 [in Stdlib.FSets.FSetCompat]
Backport_Sets.max_elt [in Stdlib.FSets.FSetCompat]
Backport_Sets.min_elt [in Stdlib.FSets.FSetCompat]
Backport_Sets.lt [in Stdlib.FSets.FSetCompat]
Backport_WSets.elements_3w [in Stdlib.FSets.FSetCompat]
Backport_WSets.elements_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.elements_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.choose_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.choose_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.partition_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.partition_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.exists_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.exists_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.for_all_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.for_all_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.filter_3 [in Stdlib.FSets.FSetCompat]
Backport_WSets.filter_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.filter_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.cardinal_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.fold_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.singleton_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.singleton_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.diff_3 [in Stdlib.FSets.FSetCompat]
Backport_WSets.diff_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.diff_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.inter_3 [in Stdlib.FSets.FSetCompat]
Backport_WSets.inter_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.inter_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.union_3 [in Stdlib.FSets.FSetCompat]
Backport_WSets.union_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.union_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.remove_3 [in Stdlib.FSets.FSetCompat]
Backport_WSets.remove_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.remove_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.add_3 [in Stdlib.FSets.FSetCompat]
Backport_WSets.add_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.add_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.is_empty_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.is_empty_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.empty_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.subset_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.subset_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.equal_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.equal_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.mem_2 [in Stdlib.FSets.FSetCompat]
Backport_WSets.mem_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.eq_trans [in Stdlib.FSets.FSetCompat]
Backport_WSets.eq_sym [in Stdlib.FSets.FSetCompat]
Backport_WSets.eq_refl [in Stdlib.FSets.FSetCompat]
Backport_WSets.In_1 [in Stdlib.FSets.FSetCompat]
Backport_WSets.choose [in Stdlib.FSets.FSetCompat]
Backport_WSets.elements [in Stdlib.FSets.FSetCompat]
Backport_WSets.cardinal [in Stdlib.FSets.FSetCompat]
Backport_WSets.partition [in Stdlib.FSets.FSetCompat]
Backport_WSets.filter [in Stdlib.FSets.FSetCompat]
Backport_WSets.exists_ [in Stdlib.FSets.FSetCompat]
Backport_WSets.for_all [in Stdlib.FSets.FSetCompat]
Backport_WSets.fold [in Stdlib.FSets.FSetCompat]
Backport_WSets.subset [in Stdlib.FSets.FSetCompat]
Backport_WSets.equal [in Stdlib.FSets.FSetCompat]
Backport_WSets.eq_dec [in Stdlib.FSets.FSetCompat]
Backport_WSets.eq [in Stdlib.FSets.FSetCompat]
Backport_WSets.diff [in Stdlib.FSets.FSetCompat]
Backport_WSets.inter [in Stdlib.FSets.FSetCompat]
Backport_WSets.union [in Stdlib.FSets.FSetCompat]
Backport_WSets.remove [in Stdlib.FSets.FSetCompat]
Backport_WSets.singleton [in Stdlib.FSets.FSetCompat]
Backport_WSets.add [in Stdlib.FSets.FSetCompat]
Backport_WSets.mem [in Stdlib.FSets.FSetCompat]
Backport_WSets.is_empty [in Stdlib.FSets.FSetCompat]
Backport_WSets.empty [in Stdlib.FSets.FSetCompat]
Backport_WSets.Exists [in Stdlib.FSets.FSetCompat]
Backport_WSets.For_all [in Stdlib.FSets.FSetCompat]
Backport_WSets.Empty [in Stdlib.FSets.FSetCompat]
Backport_WSets.Subset [in Stdlib.FSets.FSetCompat]
Backport_WSets.Equal [in Stdlib.FSets.FSetCompat]
Backport_WSets.In [in Stdlib.FSets.FSetCompat]
Backport_WSets.t [in Stdlib.FSets.FSetCompat]
Backport_WSets.elt [in Stdlib.FSets.FSetCompat]
BalanceProps.ifred [in Stdlib.MSets.MSetRBT]
BalanceProps.rbt_ind [in Stdlib.MSets.MSetRBT]
BalanceProps.redcarac [in Stdlib.MSets.MSetRBT]
BalanceProps.treeify_rb_invariant [in Stdlib.MSets.MSetRBT]
barred [in Stdlib.Logic.WeakFan]
base [in Stdlib.Numbers.Cyclic.Abstract.DoubleType]
Bcons [in Stdlib.Bool.Bvector]
bdepth [in Stdlib.micromega.ZMicromega]
Beep [in Stdlib.Strings.Ascii]
before_witness_dep_ind [in Stdlib.Logic.ConstructiveEpsilon]
before_witness_sind [in Stdlib.Logic.ConstructiveEpsilon]
before_witness_ind [in Stdlib.Logic.ConstructiveEpsilon]
beq_false_not_eq [in Stdlib.Bool.BoolEq]
beq_eq_not_false [in Stdlib.Bool.BoolEq]
beq_eq_true [in Stdlib.Bool.BoolEq]
beq_poly [in Stdlib.btauto.Algebra]
between_sind [in Stdlib.Arith.Between]
between_ind [in Stdlib.Arith.Between]
Bezout_sind [in Stdlib.ZArith.Znumtheory]
Bezout_ind [in Stdlib.ZArith.Znumtheory]
BFormula [in Stdlib.micromega.Tauto]
bFun [in Stdlib.Logic.FinFun]
Bhigh [in Stdlib.Bool.Bvector]
Bijective [in Stdlib.Logic.FinFun]
bijective_on [in Stdlib.ssr.ssrbool]
bijective_in [in Stdlib.ssr.ssrbool]
binary_normalize [in Stdlib.Floats.SpecFloat]
binary_round [in Stdlib.Floats.SpecFloat]
binary_round_aux [in Stdlib.Floats.SpecFloat]
binary_relation [in Stdlib.Classes.RelationClasses]
binary_operation [in Stdlib.Classes.RelationClasses]
bInjective [in Stdlib.Logic.FinFun]
bit [in Stdlib.Numbers.Cyclic.Int63.Uint63]
bitwise [in Stdlib.Init.Nat]
block [in Stdlib.Program.Equality]
Blow [in Stdlib.Bool.Bvector]
Bneg [in Stdlib.Bool.Bvector]
Bnil [in Stdlib.Bool.Bvector]
boolean_witness [in Stdlib.btauto.Reflect]
boolfunPredType [in Stdlib.ssr.ssrbool]
BoolOrd.compare [in Stdlib.Bool.BoolOrder]
BoolOrd.compare_spec [in Stdlib.Bool.BoolOrder]
BoolOrd.eq [in Stdlib.Bool.BoolOrder]
BoolOrd.eqb [in Stdlib.Bool.BoolOrder]
BoolOrd.eqb_eq [in Stdlib.Bool.BoolOrder]
BoolOrd.eq_trans [in Stdlib.Bool.BoolOrder]
BoolOrd.eq_sym [in Stdlib.Bool.BoolOrder]
BoolOrd.eq_refl [in Stdlib.Bool.BoolOrder]
BoolOrd.eq_dec [in Stdlib.Bool.BoolOrder]
BoolOrd.eq_equiv [in Stdlib.Bool.BoolOrder]
BoolOrd.le [in Stdlib.Bool.BoolOrder]
BoolOrd.le_lteq [in Stdlib.Bool.BoolOrder]
BoolOrd.lt [in Stdlib.Bool.BoolOrder]
BoolOrd.lt_total [in Stdlib.Bool.BoolOrder]
BoolOrd.lt_compat [in Stdlib.Bool.BoolOrder]
BoolOrd.lt_strorder [in Stdlib.Bool.BoolOrder]
BoolOrd.t [in Stdlib.Bool.BoolOrder]
BoolP [in Stdlib.Logic.ClassicalFacts]
boolP_indd [in Stdlib.Logic.ClassicalFacts]
boolP_elim_redr [in Stdlib.Logic.ClassicalFacts]
boolP_elim_redl [in Stdlib.Logic.ClassicalFacts]
boolP_sind [in Stdlib.Logic.ClassicalFacts]
boolP_ind [in Stdlib.Logic.ClassicalFacts]
BoolP_dep_induction [in Stdlib.Logic.ClassicalFacts]
BoolP_elim_redr [in Stdlib.Logic.ClassicalFacts]
BoolP_elim_redl [in Stdlib.Logic.ClassicalFacts]
BoolP_elim [in Stdlib.Logic.ClassicalFacts]
BoolSpec_sind [in Stdlib.Init.Datatypes]
BoolSpec_ind [in Stdlib.Init.Datatypes]
bool_sind [in Stdlib.Init.Datatypes]
bool_rec [in Stdlib.Init.Datatypes]
bool_ind [in Stdlib.Init.Datatypes]
bool_rect [in Stdlib.Init.Datatypes]
bool_eq [in Stdlib.setoid_ring.Ring]
bool_of_sumbool [in Stdlib.Bool.Sumbool]
bool_eq_ind [in Stdlib.Bool.Sumbool]
bool_eq_rec [in Stdlib.Bool.Sumbool]
Bottom_sind [in Stdlib.Sets.Cpo]
Bottom_rec [in Stdlib.Sets.Cpo]
Bottom_ind [in Stdlib.Sets.Cpo]
Bottom_rect [in Stdlib.Sets.Cpo]
Boule [in Stdlib.Reals.PSeries_reg]
boule_in_interval [in Stdlib.Reals.PSeries_reg]
boule_of_interval [in Stdlib.Reals.PSeries_reg]
bound [in Stdlib.Reals.Raxioms]
bounded [in Stdlib.Reals.Rtopology]
bounded [in Stdlib.Floats.SpecFloat]
bound_var [in Stdlib.micromega.ZMicromega]
BshiftL [in Stdlib.Bool.Bvector]
BshiftL_iter [in Stdlib.Bool.Bvector]
BshiftRa [in Stdlib.Bool.Bvector]
BshiftRa_iter [in Stdlib.Bool.Bvector]
BshiftRl [in Stdlib.Bool.Bvector]
BshiftRl_iter [in Stdlib.Bool.Bvector]
Bsign [in Stdlib.Bool.Bvector]
bSurjective [in Stdlib.Logic.FinFun]
build_heap_sind [in Stdlib.Sorting.Heap]
build_heap_rec [in Stdlib.Sorting.Heap]
build_heap_ind [in Stdlib.Sorting.Heap]
build_heap_rect [in Stdlib.Sorting.Heap]
Build_Setoid_Theory [in Stdlib.Setoids.Setoid]
BVand [in Stdlib.Bool.Bvector]
Bvector [in Stdlib.Bool.Bvector]
Bvect_false [in Stdlib.Bool.Bvector]
Bvect_true [in Stdlib.Bool.Bvector]
BVeq [in Stdlib.Bool.Bvector]
BVor [in Stdlib.Bool.Bvector]
BVxor [in Stdlib.Bool.Bvector]
byte_of_ascii [in Stdlib.Strings.Ascii]
byte_eq_dec [in Stdlib.Strings.Byte]
byte_of_byte [in Stdlib.Init.Byte]
byte_sind [in Stdlib.Init.Byte]
byte_rec [in Stdlib.Init.Byte]
byte_ind [in Stdlib.Init.Byte]
byte_rect [in Stdlib.Init.Byte]
B1 [in Stdlib.Reals.Cos_rel]
b2i [in Stdlib.Numbers.Cyclic.Int63.Uint63]
| 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 | (26071 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 | (1003 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 | (815 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 | (1771 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 | (589 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 | (961 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 | (12021 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 | (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 | (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 | (496 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 | (906 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 | (1204 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 | (4844 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) |