| 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 | (18986 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 | (228 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 | (297 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 | (1273 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 | (313 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 | (8135 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 | (1490 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 | (52 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |
A (variable)
AbstractConfluence.Definitions.A [in MetaRocq.PCUIC.PCUICConfluence]AbstractConfluence.Diamond.A [in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.R [in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.S [in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.sc [in MetaRocq.PCUIC.PCUICConfluence]
Acc_sidecond_generator.Pimpl [in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.P [in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.R [in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.A [in MetaRocq.SafeChecker.PCUICSafeReduce]
AllInP.A [in MetaRocq.Utils.MRList]
Alli_All_fold.A [in MetaRocq.Utils.All_Forall]
Alli_size.fn [in MetaRocq.Utils.All_Forall]
Alli_size.P [in MetaRocq.Utils.All_Forall]
Alli_size.A [in MetaRocq.Utils.All_Forall]
alli.A [in MetaRocq.Utils.All_Forall]
alli.A [in MetaRocq.Utils.All_Forall]
alli.l [in MetaRocq.Utils.All_Forall]
alli.l' [in MetaRocq.Utils.All_Forall]
alli.p [in MetaRocq.Utils.All_Forall]
alli.p [in MetaRocq.Utils.All_Forall]
alli.q [in MetaRocq.Utils.All_Forall]
All_fold.P [in MetaRocq.Utils.All_Forall]
All_fold.A [in MetaRocq.Utils.All_Forall]
All_size.fn [in MetaRocq.Utils.All_Forall]
All_size.P [in MetaRocq.Utils.All_Forall]
All_size.A [in MetaRocq.Utils.All_Forall]
All_rec.proj [in MetaRocq.Erasure.EInduction]
All_rec.A [in MetaRocq.Erasure.EInduction]
All_rec.P [in MetaRocq.Erasure.EInduction]
All2i_size.fn [in MetaRocq.Utils.All_Forall]
All2i_size.P [in MetaRocq.Utils.All_Forall]
All2i_size.B [in MetaRocq.Utils.All_Forall]
All2i_size.A [in MetaRocq.Utils.All_Forall]
All2_fold.P [in MetaRocq.Utils.All_Forall]
All2_fold.A [in MetaRocq.Utils.All_Forall]
All2_size.fn [in MetaRocq.Utils.All_Forall]
All2_size.P [in MetaRocq.Utils.All_Forall]
All2_size.B [in MetaRocq.Utils.All_Forall]
All2_size.A [in MetaRocq.Utils.All_Forall]
All2_size.fn [in MetaRocq.Erasure.EPrimitive]
All2_size.P [in MetaRocq.Erasure.EPrimitive]
All2_size.B [in MetaRocq.Erasure.EPrimitive]
All2_size.A [in MetaRocq.Erasure.EPrimitive]
Alpha.cf [in MetaRocq.PCUIC.PCUICSN]
Alpha.cf [in MetaRocq.PCUIC.PCUICAlpha]
Alpha.no [in MetaRocq.PCUIC.PCUICSN]
Alpha.normalization [in MetaRocq.PCUIC.PCUICSN]
Alpha.Σ [in MetaRocq.PCUIC.PCUICSN]
AnalyzeTop.analyze [in MetaRocq.Erasure.Typed.Optimize]
annots.A [in MetaRocq.Erasure.Typed.Annotations]
annots.lam_body_annot_cont.f [in MetaRocq.Erasure.Typed.Annotations]
annots.lam_body_annot_cont.B [in MetaRocq.Erasure.Typed.Annotations]
Arities.cf [in MetaRocq.PCUIC.PCUICClassification]
Arities.wfΣ [in MetaRocq.PCUIC.PCUICClassification]
Arities.Σ [in MetaRocq.PCUIC.PCUICClassification]
| 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 | (18986 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 | (228 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 | (297 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 | (1273 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 | (313 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 | (8135 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 | (1490 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 | (52 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |