| 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) |
T (inductive)
T [in MetaCoq.Examples.demo]TemplateMonad [in MetaCoq.Template.TemplateMonad.Core]
term [in MetaCoq.Template.Ast]
term [in MetaCoq.PCUIC.PCUICAst]
term [in MetaCoq.Erasure.EAst]
TermSpineView.t [in MetaCoq.Erasure.ESpineView]
term_direct_subterm [in MetaCoq.SafeChecker.PCUICWfReduction]
term_context [in MetaCoq.PCUIC.PCUICReduction]
TM [in MetaCoq.Template.TemplateMonad.Extractable]
tm [in MetaCoq.Examples.add_constructor]
Transitive [in MetaCoq.Translations.MiniHoTT]
Transitive [in MetaCoq.Translations.MiniHoTT_paths]
Tree.t [in MetaCoq.Template.utils.bytestring]
tsl_result [in MetaCoq.Translations.translation_utils]
tsl_error [in MetaCoq.Translations.translation_utils]
type_error [in MetaCoq.SafeChecker.PCUICErrors]
type_error [in MetaCoq.Template.Checker]
typing [in MetaCoq.Template.Typing]
typing [in MetaCoq.PCUIC.PCUICTyping]
typing_sum [in MetaCoq.PCUIC.Bidirectional.BDTyping]
typing_spine_pred [in MetaCoq.PCUIC.PCUICProgress]
typing_spine [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
typing_spine [in MetaCoq.PCUIC.PCUICArities]
typing_spine [in MetaCoq.Template.Typing]
typing_result_comp [in MetaCoq.SafeChecker.PCUICErrors]
typing_result [in MetaCoq.SafeChecker.PCUICErrors]
typing_result [in MetaCoq.Template.Checker]
typing_spine [in MetaCoq.PCUIC.PCUICGeneration]
typ_or_sort_ [in MetaCoq.Template.BasicAst]