| 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 | (19204 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 | (298 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 | (8163 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 | (1514 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 | (352 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 | (534 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 | (727 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 | (402 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 | (333 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 | (4833 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 | (182 entries) |
T (constructor)
TAny [in MetaRocq.Erasure.Typed.ExAst]TApp [in MetaRocq.Erasure.Typed.ExAst]
tApp [in MetaRocq.PCUIC.PCUICAst]
tApp [in MetaRocq.Erasure.EAst]
tApp [in MetaRocq.Template.Ast]
TArr [in MetaRocq.Erasure.Typed.ExAst]
tArray [in MetaRocq.Template.Ast]
TBox [in MetaRocq.Erasure.Typed.ExAst]
tBox [in MetaRocq.Erasure.EAst]
tCase [in MetaRocq.PCUIC.PCUICAst]
tCase [in MetaRocq.Erasure.EAst]
tCase [in MetaRocq.Template.Ast]
tCast [in MetaRocq.Template.Ast]
tCoFix [in MetaRocq.PCUIC.PCUICAst]
tCoFix [in MetaRocq.Erasure.EAst]
tCoFix [in MetaRocq.Template.Ast]
TConst [in MetaRocq.Erasure.Typed.ExAst]
tConst [in MetaRocq.PCUIC.PCUICAst]
tConst [in MetaRocq.Erasure.EAst]
tConst [in MetaRocq.Template.Ast]
tConstruct [in MetaRocq.PCUIC.PCUICAst]
tConstruct [in MetaRocq.Erasure.EAst]
tConstruct [in MetaRocq.Template.Ast]
tCtxApp_r [in MetaRocq.PCUIC.PCUICReduction]
tCtxApp_l [in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_branch [in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_discr [in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_pred [in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_pars [in MetaRocq.PCUIC.PCUICReduction]
tCtxEvar [in MetaRocq.PCUIC.PCUICReduction]
tCtxHead [in MetaRocq.PCUIC.PCUICReduction]
tCtxHead_nat [in MetaRocq.PCUIC.PCUICReduction]
tCtxHole [in MetaRocq.PCUIC.PCUICReduction]
tCtxLambda_r [in MetaRocq.PCUIC.PCUICReduction]
tCtxLambda_l [in MetaRocq.PCUIC.PCUICReduction]
tCtxLetIn_r [in MetaRocq.PCUIC.PCUICReduction]
tCtxLetIn_b [in MetaRocq.PCUIC.PCUICReduction]
tCtxLetIn_l [in MetaRocq.PCUIC.PCUICReduction]
tCtxProd_r [in MetaRocq.PCUIC.PCUICReduction]
tCtxProd_l [in MetaRocq.PCUIC.PCUICReduction]
tCtxProj [in MetaRocq.PCUIC.PCUICReduction]
tCtxTail [in MetaRocq.PCUIC.PCUICReduction]
tCtxTail_nat [in MetaRocq.PCUIC.PCUICReduction]
telescope_n_cons_def [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_cons_abs [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_nil [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope2_cons_def [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope2_cons_abs [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope2_nil [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Term [in MetaRocq.SafeChecker.PCUICSafeConversion]
TermSpineView.tApp [in MetaRocq.Erasure.ESpineView]
TermSpineView.tBox [in MetaRocq.Erasure.ESpineView]
TermSpineView.tCase [in MetaRocq.Erasure.ESpineView]
TermSpineView.tCoFix [in MetaRocq.Erasure.ESpineView]
TermSpineView.tConst [in MetaRocq.Erasure.ESpineView]
TermSpineView.tConstruct [in MetaRocq.Erasure.ESpineView]
TermSpineView.tEvar [in MetaRocq.Erasure.ESpineView]
TermSpineView.tFix [in MetaRocq.Erasure.ESpineView]
TermSpineView.tForce [in MetaRocq.Erasure.ESpineView]
TermSpineView.tLambda [in MetaRocq.Erasure.ESpineView]
TermSpineView.tLazy [in MetaRocq.Erasure.ESpineView]
TermSpineView.tLetIn [in MetaRocq.Erasure.ESpineView]
TermSpineView.tPrim [in MetaRocq.Erasure.ESpineView]
TermSpineView.tProj [in MetaRocq.Erasure.ESpineView]
TermSpineView.tRel [in MetaRocq.Erasure.ESpineView]
TermSpineView.tVar [in MetaRocq.Erasure.ESpineView]
term_direct_subterm_12_1 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_11_2 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_11_1 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_7_2 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_7_1 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_3 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_2 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_1 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_5_2 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_5_1 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_4_2 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_4_1 [in MetaRocq.SafeChecker.PCUICWfReduction]
tEvar [in MetaRocq.PCUIC.PCUICAst]
tEvar [in MetaRocq.Erasure.EAst]
tEvar [in MetaRocq.Template.Ast]
tFix [in MetaRocq.PCUIC.PCUICAst]
tFix [in MetaRocq.Erasure.EAst]
tFix [in MetaRocq.Template.Ast]
tFloat [in MetaRocq.Template.Ast]
tForce [in MetaRocq.Erasure.EAst]
Times10 [in MetaRocq.Utils.MRProd]
Times3 [in MetaRocq.Utils.MRProd]
Times4 [in MetaRocq.Utils.MRProd]
Times5 [in MetaRocq.Utils.MRProd]
Times6 [in MetaRocq.Utils.MRProd]
Times7 [in MetaRocq.Utils.MRProd]
Times8 [in MetaRocq.Utils.MRProd]
Times9 [in MetaRocq.Utils.MRProd]
TInd [in MetaRocq.Erasure.Typed.ExAst]
tInd [in MetaRocq.PCUIC.PCUICAst]
tInd [in MetaRocq.Template.Ast]
tInt [in MetaRocq.Template.Ast]
tLambda [in MetaRocq.PCUIC.PCUICAst]
tLambda [in MetaRocq.Erasure.EAst]
tLambda [in MetaRocq.Template.Ast]
tLazy [in MetaRocq.Erasure.EAst]
tLetIn [in MetaRocq.PCUIC.PCUICAst]
tLetIn [in MetaRocq.Erasure.EAst]
tLetIn [in MetaRocq.Template.Ast]
tmAxiom [in MetaRocq.Template.TemplateMonad.Extractable]
tmAxiomRed [in MetaRocq.Template.TemplateMonad.Core]
tmBind [in MetaRocq.Template.TemplateMonad.Core]
tmBind [in MetaRocq.Template.TemplateMonad.Extractable]
tmCurrentModPath [in MetaRocq.Template.TemplateMonad.Core]
tmCurrentModPath [in MetaRocq.Template.TemplateMonad.Extractable]
tmDefinitionRed_ [in MetaRocq.Template.TemplateMonad.Core]
tmDefinition_ [in MetaRocq.Template.TemplateMonad.Extractable]
tmEval [in MetaRocq.Template.TemplateMonad.Core]
tmEval [in MetaRocq.Template.TemplateMonad.Extractable]
tmExistingInstance [in MetaRocq.Template.TemplateMonad.Core]
tmExistingInstance [in MetaRocq.Template.TemplateMonad.Extractable]
tmFail [in MetaRocq.Template.TemplateMonad.Core]
tmFail [in MetaRocq.Template.TemplateMonad.Extractable]
tmFreshName [in MetaRocq.Template.TemplateMonad.Core]
tmFreshName [in MetaRocq.Template.TemplateMonad.Extractable]
tmInductive [in MetaRocq.Template.TemplateMonad.Extractable]
tmInferInstance [in MetaRocq.Template.TemplateMonad.Core]
tmInferInstance [in MetaRocq.Template.TemplateMonad.Extractable]
tmLemma [in MetaRocq.Template.TemplateMonad.Core]
tmLemma [in MetaRocq.Template.TemplateMonad.Extractable]
tmLocate [in MetaRocq.Template.TemplateMonad.Core]
tmLocate [in MetaRocq.Template.TemplateMonad.Extractable]
tmLocateModType [in MetaRocq.Template.TemplateMonad.Core]
tmLocateModType [in MetaRocq.Template.TemplateMonad.Extractable]
tmLocateModule [in MetaRocq.Template.TemplateMonad.Core]
tmLocateModule [in MetaRocq.Template.TemplateMonad.Extractable]
tmMkInductive [in MetaRocq.Template.TemplateMonad.Core]
tmMsg [in MetaRocq.Template.TemplateMonad.Core]
tmMsg [in MetaRocq.Template.TemplateMonad.Extractable]
tmPrint [in MetaRocq.Template.TemplateMonad.Core]
tmPrint [in MetaRocq.Template.TemplateMonad.Extractable]
tmQuote [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteConstant [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteConstant [in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteInductive [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteInductive [in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteModFunctor [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModFunctor [in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteModType [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModType [in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteModule [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModule [in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteRecTransp [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteUniverses [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteUniverses [in MetaRocq.Template.TemplateMonad.Extractable]
tmReturn [in MetaRocq.Template.TemplateMonad.Core]
tmReturn [in MetaRocq.Template.TemplateMonad.Extractable]
tmUnquote [in MetaRocq.Template.TemplateMonad.Core]
tmUnquoteTyped [in MetaRocq.Template.TemplateMonad.Core]
tmVariable [in MetaRocq.Template.TemplateMonad.Core]
toplevel_and_submodules [in MetaRocq.Quotation.ToPCUIC.Init]
toplevel_and_submodules [in MetaRocq.Quotation.ToTemplate.Init]
toto [in MetaRocq.Examples.demo]
tPrim [in MetaRocq.PCUIC.PCUICAst]
tPrim [in MetaRocq.Erasure.EAst]
tProd [in MetaRocq.PCUIC.PCUICAst]
tProd [in MetaRocq.Template.Ast]
tProj [in MetaRocq.PCUIC.PCUICAst]
tProj [in MetaRocq.Erasure.EAst]
tProj [in MetaRocq.Template.Ast]
Tr [in MetaRocq.Examples.tauto]
TransformExt.preserves_obs [in MetaRocq.Erasure.EProgram]
trans_red [in MetaRocq.Template.Typing]
trans_redl [in MetaRocq.PCUIC.PCUICReduction]
Tree.append [in MetaRocq.Utils.bytestring]
Tree.string [in MetaRocq.Utils.bytestring]
tRel [in MetaRocq.PCUIC.PCUICAst]
tRel [in MetaRocq.Erasure.EAst]
tRel [in MetaRocq.Template.Ast]
tSort [in MetaRocq.PCUIC.PCUICAst]
tSort [in MetaRocq.Template.Ast]
tString [in MetaRocq.Template.Ast]
TVar [in MetaRocq.Erasure.Typed.ExAst]
tVar [in MetaRocq.PCUIC.PCUICAst]
tVar [in MetaRocq.Erasure.EAst]
tVar [in MetaRocq.Template.Ast]
TypeAliasDecl [in MetaRocq.Erasure.Typed.ExAst]
TypeError [in MetaRocq.SafeChecker.PCUICErrors]
TypeError [in MetaRocq.Template.Checker]
TypeError_comp [in MetaRocq.SafeChecker.PCUICErrors]
type_spine_cons [in MetaRocq.PCUIC.PCUICGeneration]
type_spine_nil [in MetaRocq.PCUIC.PCUICGeneration]
type_Cumul [in MetaRocq.PCUIC.PCUICTyping]
type_Prim [in MetaRocq.PCUIC.PCUICTyping]
type_CoFix [in MetaRocq.PCUIC.PCUICTyping]
type_Fix [in MetaRocq.PCUIC.PCUICTyping]
type_Proj [in MetaRocq.PCUIC.PCUICTyping]
type_Case [in MetaRocq.PCUIC.PCUICTyping]
type_Construct [in MetaRocq.PCUIC.PCUICTyping]
type_Ind [in MetaRocq.PCUIC.PCUICTyping]
type_Const [in MetaRocq.PCUIC.PCUICTyping]
type_App [in MetaRocq.PCUIC.PCUICTyping]
type_LetIn [in MetaRocq.PCUIC.PCUICTyping]
type_Lambda [in MetaRocq.PCUIC.PCUICTyping]
type_Prod [in MetaRocq.PCUIC.PCUICTyping]
type_Sort [in MetaRocq.PCUIC.PCUICTyping]
type_Rel [in MetaRocq.PCUIC.PCUICTyping]
type_spine_cons [in MetaRocq.PCUIC.PCUICArities]
type_spine_nil [in MetaRocq.PCUIC.PCUICArities]
type_spine_pred_cons [in MetaRocq.PCUIC.PCUICProgress]
type_spine_pred_nil [in MetaRocq.PCUIC.PCUICProgress]
type_spine_cons [in MetaRocq.Template.Typing]
type_spine_nil [in MetaRocq.Template.Typing]
type_Conv [in MetaRocq.Template.Typing]
type_Array [in MetaRocq.Template.Typing]
type_String [in MetaRocq.Template.Typing]
type_Float [in MetaRocq.Template.Typing]
type_Int [in MetaRocq.Template.Typing]
type_CoFix [in MetaRocq.Template.Typing]
type_Fix [in MetaRocq.Template.Typing]
type_Proj [in MetaRocq.Template.Typing]
type_Case [in MetaRocq.Template.Typing]
type_Construct [in MetaRocq.Template.Typing]
type_Ind [in MetaRocq.Template.Typing]
type_Const [in MetaRocq.Template.Typing]
type_App [in MetaRocq.Template.Typing]
type_LetIn [in MetaRocq.Template.Typing]
type_Lambda [in MetaRocq.Template.Typing]
type_Prod [in MetaRocq.Template.Typing]
type_Cast [in MetaRocq.Template.Typing]
type_Sort [in MetaRocq.Template.Typing]
type_Rel [in MetaRocq.Template.Typing]
type_spine_cons [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_spine_nil [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_spine_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
| 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 | (19204 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 | (298 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 | (8163 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 | (1514 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 | (352 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 | (534 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 | (727 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 | (402 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 | (333 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 | (4833 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 | (182 entries) |