| 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 | (75519 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 | (245 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
E (section)
EEnvFlags [in MetaCoq.Erasure.EWellformed]EEnvFlags [in MetaCoq.Erasure.EExtends]
Elim' [in MetaCoq.Erasure.EArities]
EnvCheck [in MetaCoq.SafeChecker.PCUICErrors]
EnvMap.Poly [in MetaCoq.Template.EnvMap]
EnvTyping.All_local_env_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_rel [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.Bidirectional [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.Regular [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.TypeCtxInst [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.TypeLocal [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.TypeLocalOver [in MetaCoq.Template.EnvironmentTyping]
EqualityDec [in MetaCoq.SafeChecker.PCUICEqualityDec]
EqualityLemmas [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
EquivInverse [in MetaCoq.Translations.MiniHoTT]
EquivInverse [in MetaCoq.Translations.MiniHoTT_paths]
EquivTransport [in MetaCoq.Translations.MiniHoTT]
EquivTransport [in MetaCoq.Translations.MiniHoTT_paths]
eq_list [in MetaCoq.Template.utils.ReflectEq]
Erase [in MetaCoq.Erasure.ErasureFunction]
EraseGlobalFast [in MetaCoq.Erasure.ErasureFunction]
Eta [in MetaCoq.Template.EtaExpand]
eval_mkApps_rect [in MetaCoq.Erasure.EWcbvEvalInd]
expanded [in MetaCoq.Template.EtaExpand]
expanded [in MetaCoq.Erasure.EEtaExpandedFix]
expanded [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded [in MetaCoq.Erasure.EEtaExpanded]
ExtendsWf [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ExtendsWf [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]