| 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 | (70451 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) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |
M (axiom)
make [in Coq.Array.PArray]max_length [in Coq.Array.PArray]
MiniDecidableType.eq_dec [in Coq.Structures.Equalities]
MiniOrderedType.compare [in Coq.Structures.OrderedType]
MiniOrderedType.eq [in Coq.Structures.OrderedType]
MiniOrderedType.eq_trans [in Coq.Structures.OrderedType]
MiniOrderedType.eq_sym [in Coq.Structures.OrderedType]
MiniOrderedType.eq_refl [in Coq.Structures.OrderedType]
MiniOrderedType.lt [in Coq.Structures.OrderedType]
MiniOrderedType.lt_not_eq [in Coq.Structures.OrderedType]
MiniOrderedType.lt_trans [in Coq.Structures.OrderedType]
MiniOrderedType.t [in Coq.Structures.OrderedType]
mod [in Coq.Numbers.Cyclic.Int63.Int63]
mod_spec [in Coq.Numbers.Cyclic.Int63.Int63]
MSetRemoveMin.remove_min_spec2 [in Coq.MSets.MSetRBT]
MSetRemoveMin.remove_min_spec1 [in Coq.MSets.MSetRBT]
MSetRemoveMin.remove_min [in Coq.MSets.MSetRBT]
mul [in Coq.Floats.PrimFloat]
mul [in Coq.Numbers.Cyclic.Int63.Int63]
mulc [in Coq.Numbers.Cyclic.Int63.Int63]
mulc_spec [in Coq.Numbers.Cyclic.Int63.Int63]
mul_spec [in Coq.Numbers.Cyclic.Int63.Int63]
mul_spec [in Coq.Floats.FloatAxioms]
