| 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 (constructor)
tApp [in MetaCoq.Template.Ast]tApp [in MetaCoq.PCUIC.PCUICAst]
tApp [in MetaCoq.Erasure.EAst]
tBox [in MetaCoq.Erasure.EAst]
tCase [in MetaCoq.Template.Ast]
tCase [in MetaCoq.PCUIC.PCUICAst]
tCase [in MetaCoq.Erasure.EAst]
tCast [in MetaCoq.Template.Ast]
tCoFix [in MetaCoq.Template.Ast]
tCoFix [in MetaCoq.PCUIC.PCUICAst]
tCoFix [in MetaCoq.Erasure.EAst]
tConst [in MetaCoq.Template.Ast]
tConst [in MetaCoq.PCUIC.PCUICAst]
tConst [in MetaCoq.Erasure.EAst]
tConstruct [in MetaCoq.Template.Ast]
tConstruct [in MetaCoq.PCUIC.PCUICAst]
tConstruct [in MetaCoq.Erasure.EAst]
tCtxApp_r [in MetaCoq.PCUIC.PCUICReduction]
tCtxApp_l [in MetaCoq.PCUIC.PCUICReduction]
tCtxCase_branch [in MetaCoq.PCUIC.PCUICReduction]
tCtxCase_discr [in MetaCoq.PCUIC.PCUICReduction]
tCtxCase_pred [in MetaCoq.PCUIC.PCUICReduction]
tCtxCase_pars [in MetaCoq.PCUIC.PCUICReduction]
tCtxEvar [in MetaCoq.PCUIC.PCUICReduction]
tCtxHead [in MetaCoq.PCUIC.PCUICReduction]
tCtxHead_nat [in MetaCoq.PCUIC.PCUICReduction]
tCtxHole [in MetaCoq.PCUIC.PCUICReduction]
tCtxLambda_r [in MetaCoq.PCUIC.PCUICReduction]
tCtxLambda_l [in MetaCoq.PCUIC.PCUICReduction]
tCtxLetIn_r [in MetaCoq.PCUIC.PCUICReduction]
tCtxLetIn_b [in MetaCoq.PCUIC.PCUICReduction]
tCtxLetIn_l [in MetaCoq.PCUIC.PCUICReduction]
tCtxProd_r [in MetaCoq.PCUIC.PCUICReduction]
tCtxProd_l [in MetaCoq.PCUIC.PCUICReduction]
tCtxProj [in MetaCoq.PCUIC.PCUICReduction]
tCtxTail [in MetaCoq.PCUIC.PCUICReduction]
tCtxTail_nat [in MetaCoq.PCUIC.PCUICReduction]
telescope_n_cons_def [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_cons_abs [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_nil [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
telescope2_cons_def [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
telescope2_cons_abs [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
telescope2_nil [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Term [in MetaCoq.SafeChecker.PCUICSafeConversion]
TermSpineView.tApp [in MetaCoq.Erasure.ESpineView]
TermSpineView.tBox [in MetaCoq.Erasure.ESpineView]
TermSpineView.tCase [in MetaCoq.Erasure.ESpineView]
TermSpineView.tCoFix [in MetaCoq.Erasure.ESpineView]
TermSpineView.tConst [in MetaCoq.Erasure.ESpineView]
TermSpineView.tConstruct [in MetaCoq.Erasure.ESpineView]
TermSpineView.tEvar [in MetaCoq.Erasure.ESpineView]
TermSpineView.tFix [in MetaCoq.Erasure.ESpineView]
TermSpineView.tLambda [in MetaCoq.Erasure.ESpineView]
TermSpineView.tLetIn [in MetaCoq.Erasure.ESpineView]
TermSpineView.tProj [in MetaCoq.Erasure.ESpineView]
TermSpineView.tRel [in MetaCoq.Erasure.ESpineView]
TermSpineView.tVar [in MetaCoq.Erasure.ESpineView]
term_direct_subterm_12_1 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_11_2 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_11_1 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_7_2 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_7_1 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_3 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_2 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_1 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_5_2 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_5_1 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_4_2 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_4_1 [in MetaCoq.SafeChecker.PCUICWfReduction]
tEvar [in MetaCoq.Template.Ast]
tEvar [in MetaCoq.PCUIC.PCUICAst]
tEvar [in MetaCoq.Erasure.EAst]
tFix [in MetaCoq.Template.Ast]
tFix [in MetaCoq.PCUIC.PCUICAst]
tFix [in MetaCoq.Erasure.EAst]
Times10 [in MetaCoq.Template.utils.MCProd]
Times3 [in MetaCoq.Template.utils.MCProd]
Times4 [in MetaCoq.Template.utils.MCProd]
Times5 [in MetaCoq.Template.utils.MCProd]
Times6 [in MetaCoq.Template.utils.MCProd]
Times7 [in MetaCoq.Template.utils.MCProd]
Times8 [in MetaCoq.Template.utils.MCProd]
Times9 [in MetaCoq.Template.utils.MCProd]
tInd [in MetaCoq.Template.Ast]
tInd [in MetaCoq.PCUIC.PCUICAst]
tLambda [in MetaCoq.Template.Ast]
tLambda [in MetaCoq.PCUIC.PCUICAst]
tLambda [in MetaCoq.Erasure.EAst]
tLetIn [in MetaCoq.Template.Ast]
tLetIn [in MetaCoq.PCUIC.PCUICAst]
tLetIn [in MetaCoq.Erasure.EAst]
tmAxiom [in MetaCoq.Template.TemplateMonad.Extractable]
tmAxiomRed [in MetaCoq.Template.TemplateMonad.Core]
tmBind [in MetaCoq.Template.TemplateMonad.Core]
tmBind [in MetaCoq.Template.TemplateMonad.Extractable]
tmCurrentModPath [in MetaCoq.Template.TemplateMonad.Core]
tmCurrentModPath [in MetaCoq.Template.TemplateMonad.Extractable]
tmDefinitionRed_ [in MetaCoq.Template.TemplateMonad.Core]
tmDefinition_ [in MetaCoq.Template.TemplateMonad.Extractable]
tmEval [in MetaCoq.Template.TemplateMonad.Core]
tmEval [in MetaCoq.Template.TemplateMonad.Extractable]
tmExistingInstance [in MetaCoq.Template.TemplateMonad.Core]
tmExistingInstance [in MetaCoq.Template.TemplateMonad.Extractable]
tmFail [in MetaCoq.Template.TemplateMonad.Core]
tmFail [in MetaCoq.Template.TemplateMonad.Extractable]
tmFreshName [in MetaCoq.Template.TemplateMonad.Core]
tmFreshName [in MetaCoq.Template.TemplateMonad.Extractable]
tmInductive [in MetaCoq.Template.TemplateMonad.Extractable]
tmInferInstance [in MetaCoq.Template.TemplateMonad.Core]
tmInferInstance [in MetaCoq.Template.TemplateMonad.Extractable]
tmLemma [in MetaCoq.Template.TemplateMonad.Core]
tmLemma [in MetaCoq.Template.TemplateMonad.Extractable]
tmLocate [in MetaCoq.Template.TemplateMonad.Core]
tmLocate [in MetaCoq.Template.TemplateMonad.Extractable]
tmMkInductive [in MetaCoq.Template.TemplateMonad.Core]
tmMsg [in MetaCoq.Template.TemplateMonad.Core]
tmMsg [in MetaCoq.Template.TemplateMonad.Extractable]
tmPrint [in MetaCoq.Template.TemplateMonad.Core]
tmPrint [in MetaCoq.Template.TemplateMonad.Extractable]
tmQuote [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteConstant [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteConstant [in MetaCoq.Template.TemplateMonad.Extractable]
tmQuoteInductive [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteInductive [in MetaCoq.Template.TemplateMonad.Extractable]
tmQuoteModule [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteModule [in MetaCoq.Template.TemplateMonad.Extractable]
tmQuoteRecTransp [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteUniverses [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteUniverses [in MetaCoq.Template.TemplateMonad.Extractable]
tmReturn [in MetaCoq.Template.TemplateMonad.Core]
tmReturn [in MetaCoq.Template.TemplateMonad.Extractable]
tmUnquote [in MetaCoq.Template.TemplateMonad.Core]
tmUnquoteTyped [in MetaCoq.Template.TemplateMonad.Core]
tmVariable [in MetaCoq.Template.TemplateMonad.Core]
toto [in MetaCoq.Examples.demo]
tProd [in MetaCoq.Template.Ast]
tProd [in MetaCoq.PCUIC.PCUICAst]
tProj [in MetaCoq.Template.Ast]
tProj [in MetaCoq.PCUIC.PCUICAst]
tProj [in MetaCoq.Erasure.EAst]
Tr [in MetaCoq.Examples.tauto]
transitivity [in MetaCoq.Translations.MiniHoTT]
transitivity [in MetaCoq.Translations.MiniHoTT_paths]
TranslationNotFound [in MetaCoq.Translations.translation_utils]
TranslationNotHandeled [in MetaCoq.Translations.translation_utils]
trans_red [in MetaCoq.Template.Typing]
trans_redl [in MetaCoq.PCUIC.PCUICReduction]
Tree.append [in MetaCoq.Template.utils.bytestring]
Tree.string [in MetaCoq.Template.utils.bytestring]
tRel [in MetaCoq.Template.Ast]
tRel [in MetaCoq.PCUIC.PCUICAst]
tRel [in MetaCoq.Erasure.EAst]
tSort [in MetaCoq.Template.Ast]
tSort [in MetaCoq.PCUIC.PCUICAst]
tVar [in MetaCoq.Template.Ast]
tVar [in MetaCoq.PCUIC.PCUICAst]
tVar [in MetaCoq.Erasure.EAst]
Typ [in MetaCoq.Template.BasicAst]
TypeError [in MetaCoq.SafeChecker.PCUICErrors]
TypeError [in MetaCoq.Template.Checker]
TypeError_comp [in MetaCoq.SafeChecker.PCUICErrors]
type_spine_pred_cons [in MetaCoq.PCUIC.PCUICProgress]
type_spine_pred_nil [in MetaCoq.PCUIC.PCUICProgress]
type_spine_cons [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
type_spine_nil [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
type_spine_eq [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
type_spine_cons [in MetaCoq.PCUIC.PCUICArities]
type_spine_nil [in MetaCoq.PCUIC.PCUICArities]
type_spine_cons [in MetaCoq.Template.Typing]
type_spine_nil [in MetaCoq.Template.Typing]
type_Conv [in MetaCoq.Template.Typing]
type_CoFix [in MetaCoq.Template.Typing]
type_Fix [in MetaCoq.Template.Typing]
type_Proj [in MetaCoq.Template.Typing]
type_Case [in MetaCoq.Template.Typing]
type_Construct [in MetaCoq.Template.Typing]
type_Ind [in MetaCoq.Template.Typing]
type_Const [in MetaCoq.Template.Typing]
type_App [in MetaCoq.Template.Typing]
type_LetIn [in MetaCoq.Template.Typing]
type_Lambda [in MetaCoq.Template.Typing]
type_Prod [in MetaCoq.Template.Typing]
type_Cast [in MetaCoq.Template.Typing]
type_Sort [in MetaCoq.Template.Typing]
type_Rel [in MetaCoq.Template.Typing]
type_spine_cons [in MetaCoq.PCUIC.PCUICGeneration]
type_spine_nil [in MetaCoq.PCUIC.PCUICGeneration]
type_Cumul [in MetaCoq.PCUIC.PCUICTyping]
type_CoFix [in MetaCoq.PCUIC.PCUICTyping]
type_Fix [in MetaCoq.PCUIC.PCUICTyping]
type_Proj [in MetaCoq.PCUIC.PCUICTyping]
type_Case [in MetaCoq.PCUIC.PCUICTyping]
type_Construct [in MetaCoq.PCUIC.PCUICTyping]
type_Ind [in MetaCoq.PCUIC.PCUICTyping]
type_Const [in MetaCoq.PCUIC.PCUICTyping]
type_App [in MetaCoq.PCUIC.PCUICTyping]
type_LetIn [in MetaCoq.PCUIC.PCUICTyping]
type_Lambda [in MetaCoq.PCUIC.PCUICTyping]
type_Prod [in MetaCoq.PCUIC.PCUICTyping]
type_Sort [in MetaCoq.PCUIC.PCUICTyping]
type_Rel [in MetaCoq.PCUIC.PCUICTyping]
TypingError [in MetaCoq.Translations.translation_utils]
| 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) |