| 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 (definition)
tAnd [in MetaRocq.Examples.tauto]target_wcbv_flags [in MetaRocq.Erasure.EWcbvEval]
tauto_s [in MetaRocq.Examples.tauto]
tauto_proc [in MetaRocq.Examples.tauto]
tCaseBrsProp [in MetaRocq.PCUIC.PCUICAst]
tCaseBrsProp [in MetaRocq.Template.Ast]
tCaseBrsProp_k [in MetaRocq.PCUIC.PCUICAst]
tCaseBrsType [in MetaRocq.Template.AstUtils]
tCasePredProp [in MetaRocq.PCUIC.PCUICAst]
tCasePredProp [in MetaRocq.Template.Ast]
tCasePredProp_k [in MetaRocq.PCUIC.PCUICAst]
tDummy [in MetaRocq.PCUIC.utils.PCUICOnOne]
tDummy [in MetaRocq.Template.Ast]
telescope [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
TemplateConversionPar.cumul_gen [in MetaRocq.Template.Typing]
TemplateMonad_Monad [in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_OptimizedMonad [in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_UnoptimizedMonad [in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_sind [in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_ind [in MetaRocq.Template.TemplateMonad.Core]
TemplateTermUtils.destArity [in MetaRocq.Template.Ast]
TemplateTermUtils.inds [in MetaRocq.Template.Ast]
TemplateTerm.closedn [in MetaRocq.Template.Ast]
TemplateTerm.lift [in MetaRocq.Template.Ast]
TemplateTerm.mkApps [in MetaRocq.Template.Ast]
TemplateTerm.noccur_between [in MetaRocq.Template.Ast]
TemplateTerm.subst [in MetaRocq.Template.Ast]
TemplateTerm.subst_instance_constr [in MetaRocq.Template.Ast]
TemplateTerm.term [in MetaRocq.Template.Ast]
TemplateTerm.tInd [in MetaRocq.Template.Ast]
TemplateTerm.tLambda [in MetaRocq.Template.Ast]
TemplateTerm.tLetIn [in MetaRocq.Template.Ast]
TemplateTerm.tProd [in MetaRocq.Template.Ast]
TemplateTerm.tProj [in MetaRocq.Template.Ast]
TemplateTerm.tRel [in MetaRocq.Template.Ast]
TemplateTerm.tSort [in MetaRocq.Template.Ast]
TemplateTransform [in MetaRocq.Erasure.Typed.Transform]
TemplateTyping.typing [in MetaRocq.Template.Typing]
template_program_env [in MetaRocq.Template.TemplateProgram]
template_program [in MetaRocq.Template.TemplateProgram]
template_eta [in MetaRocq.Erasure.Typed.CertifyingEta]
template_betared [in MetaRocq.Erasure.Typed.CertifyingBeta]
template_to_pcuic_mapping [in MetaRocq.ErasurePlugin.Erasure]
template_to_pcuic_transform [in MetaRocq.TemplatePCUIC.PCUICTransform]
template_inline [in MetaRocq.Erasure.Typed.CertifyingInlining]
TermSpineView.t_sind [in MetaRocq.Erasure.ESpineView]
TermSpineView.t_rec [in MetaRocq.Erasure.ESpineView]
TermSpineView.t_ind [in MetaRocq.Erasure.ESpineView]
TermSpineView.t_rect [in MetaRocq.Erasure.ESpineView]
TermSpineView.view [in MetaRocq.Erasure.ESpineView]
term_sub_ctx_sind [in MetaRocq.Erasure.Typed.Erasure]
term_sub_ctx_ind [in MetaRocq.Erasure.Typed.Erasure]
term_rel [in MetaRocq.Erasure.ErasureFunction]
term_flags [in MetaRocq.Erasure.EWcbvEvalEtaInd]
term_sind [in MetaRocq.PCUIC.PCUICAst]
term_rec [in MetaRocq.PCUIC.PCUICAst]
term_ind [in MetaRocq.PCUIC.PCUICAst]
term_rect [in MetaRocq.PCUIC.PCUICAst]
term_sind [in MetaRocq.Erasure.EAst]
term_rec [in MetaRocq.Erasure.EAst]
term_ind [in MetaRocq.Erasure.EAst]
term_rect [in MetaRocq.Erasure.EAst]
term_context_sind [in MetaRocq.PCUIC.PCUICReduction]
term_context_rec [in MetaRocq.PCUIC.PCUICReduction]
term_context_ind [in MetaRocq.PCUIC.PCUICReduction]
term_context_rect [in MetaRocq.PCUIC.PCUICReduction]
term_subterm_wf [in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm_context [in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_context [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_sind [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_rec [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_ind [in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_rect [in MetaRocq.SafeChecker.PCUICWfReduction]
term_eqb [in MetaRocq.Template.Lib]
term_sind [in MetaRocq.Template.Ast]
term_rec [in MetaRocq.Template.Ast]
term_ind [in MetaRocq.Template.Ast]
term_rect [in MetaRocq.Template.Ast]
term_global_deps [in MetaRocq.Erasure.EAstUtils]
test [in MetaRocq.Examples.add_constructor]
test [in MetaRocq.Examples.metarocq_tour]
test_branch_k_pars [in MetaRocq.PCUIC.Syntax.PCUICPosition]
test_context_k [in MetaRocq.Common.BasicAst]
test_context [in MetaRocq.Common.BasicAst]
test_decl [in MetaRocq.Common.BasicAst]
test_def [in MetaRocq.Common.BasicAst]
test_branches_nlict [in MetaRocq.PCUIC.PCUICAst]
test_branch_nlict [in MetaRocq.PCUIC.PCUICAst]
test_context_nlict [in MetaRocq.PCUIC.PCUICAst]
test_branch_k [in MetaRocq.PCUIC.PCUICAst]
test_branch [in MetaRocq.PCUIC.PCUICAst]
test_predicate_ku [in MetaRocq.PCUIC.PCUICAst]
test_predicate_k [in MetaRocq.PCUIC.PCUICAst]
test_predicate [in MetaRocq.PCUIC.PCUICAst]
test_def [in MetaRocq.Erasure.EAst]
test_snd [in MetaRocq.Utils.MRProd]
test_branch [in MetaRocq.Template.Ast]
test_predicate_k [in MetaRocq.Template.Ast]
test_predicate [in MetaRocq.Template.Ast]
test_primIn [in MetaRocq.Erasure.EPrimitive]
test_prim [in MetaRocq.Erasure.EPrimitive]
test_array_model [in MetaRocq.Erasure.EPrimitive]
test_primu [in MetaRocq.PCUIC.utils.PCUICPrimitive]
test_prim [in MetaRocq.PCUIC.utils.PCUICPrimitive]
test' [in MetaRocq.Examples.add_constructor]
test2 [in MetaRocq.Examples.add_constructor]
test3 [in MetaRocq.Examples.add_constructor]
test4 [in MetaRocq.Examples.add_constructor]
tFixCoFix [in MetaRocq.PCUIC.PCUICGuardCondition]
tFixProp [in MetaRocq.Common.BasicAst]
tFixType [in MetaRocq.Template.AstUtils]
throwIf [in MetaRocq.Erasure.Typed.Optimize]
time [in MetaRocq.Common.Transform]
timed [in MetaRocq.Erasure.Typed.Utils]
tImpl [in MetaRocq.Examples.tauto]
tImpl [in MetaRocq.Examples.typing_correctness]
tImpl [in MetaRocq.Examples.metarocq_tour_prelude]
tmAxiom [in MetaRocq.Template.TemplateMonad.Core]
tmAxiomRed [in MetaRocq.Template.TemplateMonad.Extractable]
tmDeclareQuotationOfConstants [in MetaRocq.Quotation.ToPCUIC.Init]
tmDeclareQuotationOfConstants [in MetaRocq.Quotation.ToTemplate.Init]
tmDeclareQuotationOfModule [in MetaRocq.Quotation.ToPCUIC.Init]
tmDeclareQuotationOfModule [in MetaRocq.Quotation.ToTemplate.Init]
tmDefinition [in MetaRocq.Template.TemplateMonad.Core]
tmDefinition [in MetaRocq.Template.TemplateMonad.Extractable]
tmDefinitionRed [in MetaRocq.Template.TemplateMonad.Core]
tmDefinitionRed [in MetaRocq.Template.TemplateMonad.Extractable]
tmFix [in MetaRocq.Template.TemplateMonad.Core]
tmFix' [in MetaRocq.Template.TemplateMonad.Core]
tmInductive' [in MetaRocq.Template.TemplateMonad.Extractable]
tmInferInstanceRed [in MetaRocq.Template.TemplateMonad.Extractable]
tmLemmaRed [in MetaRocq.Template.TemplateMonad.Extractable]
tmLocateInd [in MetaRocq.Examples.tauto]
tmLocateModType1 [in MetaRocq.Template.TemplateMonad.Core]
tmLocateModule1 [in MetaRocq.Template.TemplateMonad.Core]
tmLocate1 [in MetaRocq.Template.TemplateMonad.Core]
tmMakeQuotationOfConstants [in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfConstants [in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfConstantsWorkAroundRocqBug17303 [in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfConstantsWorkAroundRocqBug17303 [in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfConstants_gen [in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfConstants_gen [in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfModule [in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfModule [in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfModuleWorkAroundRocqBug17303 [in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfModuleWorkAroundRocqBug17303 [in MetaRocq.Quotation.ToTemplate.Init]
tmMaybeEval [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
tmMkDefinition [in MetaRocq.Template.TemplateMonad.Core]
tmMkDefinition [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmMkInductive [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmMkInductive' [in MetaRocq.Template.TemplateMonad.Core]
tmOpaqueDefinition [in MetaRocq.Template.TemplateMonad.Extractable]
tmOpaqueDefinitionRed [in MetaRocq.Template.TemplateMonad.Core]
tmOptimize [in MetaRocq.Template.TemplateMonad.Core]
tmOptimizedBind [in MetaRocq.Template.TemplateMonad.Core]
tmOptimize' [in MetaRocq.Template.TemplateMonad.Core]
tmQuote [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteConstant [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteDefinition [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteDefinitionRed [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteInductive [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
tmQuoteInductive [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteInductive' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
tmQuoteLevel [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteRec [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteRec [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteRecDefinition [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteRecTransp [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteSort [in MetaRocq.Template.TemplateMonad.Core]
tmQuoteUniverse [in MetaRocq.Template.TemplateMonad.Core]
tmTestQuote [in MetaRocq.Template.TemplateMonad.Core]
tmTestUnquote [in MetaRocq.Template.TemplateMonad.Core]
tmUnquote [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmUnquoteTyped [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tm_sind [in MetaRocq.Examples.add_constructor]
tm_rec [in MetaRocq.Examples.add_constructor]
tm_ind [in MetaRocq.Examples.add_constructor]
tm_rect [in MetaRocq.Examples.add_constructor]
TM_sind [in MetaRocq.Template.TemplateMonad.Extractable]
TM_rec [in MetaRocq.Template.TemplateMonad.Extractable]
TM_ind [in MetaRocq.Template.TemplateMonad.Extractable]
TM_rect [in MetaRocq.Template.TemplateMonad.Extractable]
tOr [in MetaRocq.Examples.tauto]
to_kername [in MetaRocq.Erasure.Typed.Utils]
to_program [in MetaRocq.ErasurePlugin.ETransform]
tPrimProp [in MetaRocq.PCUIC.utils.PCUICPrimitive]
trans [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans [in MetaRocq.PCUIC.PCUICExpandLets]
trans [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans [in MetaRocq.Erasure.ECoInductiveToInductive]
Transform [in MetaRocq.Erasure.Typed.Transform]
transform_blocks_program [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_env [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_decl [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_constant_decl [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_compose [in MetaRocq.ErasurePlugin.Erasure]
Transform.compose [in MetaRocq.Common.Transform]
Transform.preserves_eval [in MetaRocq.Common.Transform]
Transform.program [in MetaRocq.Common.Transform]
Transform.run [in MetaRocq.Common.Transform]
Transform.self_transform [in MetaRocq.Common.Transform]
TransLookup_lookup_inductive' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
TransLookup.lookup_inductive [in MetaRocq.PCUIC.PCUICProgram]
TransLookup.lookup_minductive [in MetaRocq.PCUIC.PCUICProgram]
transport [in MetaRocq.Utils.MREquality]
transport_ws_term [in MetaRocq.PCUIC.PCUICConfluence]
transport_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
trans_env [in MetaRocq.Erasure.Typed.ExAst]
trans_global_decl [in MetaRocq.Erasure.Typed.ExAst]
trans_mib [in MetaRocq.Erasure.Typed.ExAst]
trans_oib [in MetaRocq.Erasure.Typed.ExAst]
trans_ctors [in MetaRocq.Erasure.Typed.ExAst]
trans_cst [in MetaRocq.Erasure.Typed.ExAst]
trans_template_program [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global_env [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global_decls [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global_decl [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_minductive_body [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_constant_body [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_one_ind_body [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_projection_body [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_constructor_body [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_local [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_decl [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_branch [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_predicate [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global [in MetaRocq.PCUIC.PCUICExpandLets]
trans_global_env [in MetaRocq.PCUIC.PCUICExpandLets]
trans_global_decls [in MetaRocq.PCUIC.PCUICExpandLets]
trans_global_decl [in MetaRocq.PCUIC.PCUICExpandLets]
trans_constant_body [in MetaRocq.PCUIC.PCUICExpandLets]
trans_minductive_body [in MetaRocq.PCUIC.PCUICExpandLets]
trans_one_ind_body [in MetaRocq.PCUIC.PCUICExpandLets]
trans_projection_body [in MetaRocq.PCUIC.PCUICExpandLets]
trans_constructor_body [in MetaRocq.PCUIC.PCUICExpandLets]
trans_cstr_concl [in MetaRocq.PCUIC.PCUICExpandLets]
trans_cstr_concl_head [in MetaRocq.PCUIC.PCUICExpandLets]
trans_local [in MetaRocq.PCUIC.PCUICExpandLets]
trans_branch [in MetaRocq.PCUIC.PCUICExpandLets]
trans_def [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_program [in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
trans_ex_prog [in MetaRocq.ErasurePlugin.ETransform]
trans_mutual_inductive_entry [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_one_inductive_entry [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global_env [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global_decls [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global_decl [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_minductive_body [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_constant_body [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_one_ind_body [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_projection_body [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_constructor_body [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_local [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_branch [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_predicate [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_prim [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_def [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_program_expanded [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_program_wf [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_program [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env' [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_decl [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_constant_decl [in MetaRocq.Erasure.ECoInductiveToInductive]
traverse_env [in MetaRocq.Erasure.Typed.Certifying]
Tree.concat [in MetaRocq.Utils.bytestring]
Tree.parens [in MetaRocq.Utils.bytestring]
Tree.print_list [in MetaRocq.Utils.bytestring]
Tree.string_of_list [in MetaRocq.Utils.bytestring]
Tree.string_of_list_aux [in MetaRocq.Utils.bytestring]
Tree.to_string [in MetaRocq.Utils.bytestring]
Tree.to_string_acc [in MetaRocq.Utils.bytestring]
Tree.to_rev_list_aux [in MetaRocq.Utils.bytestring]
Tree.t_sind [in MetaRocq.Utils.bytestring]
Tree.t_rec [in MetaRocq.Utils.bytestring]
Tree.t_ind [in MetaRocq.Utils.bytestring]
Tree.t_rect [in MetaRocq.Utils.bytestring]
tRel_kind_sind [in MetaRocq.Erasure.Typed.Erasure]
tRel_kind_rec [in MetaRocq.Erasure.Typed.Erasure]
tRel_kind_ind [in MetaRocq.Erasure.Typed.Erasure]
tRel_kind_rect [in MetaRocq.Erasure.Typed.Erasure]
trim_ind_masks [in MetaRocq.Erasure.Typed.Optimize]
trim_mib_masks [in MetaRocq.Erasure.Typed.Optimize]
trim_ctor_masks [in MetaRocq.Erasure.Typed.Optimize]
trim_const_masks [in MetaRocq.Erasure.Typed.Optimize]
trim_end [in MetaRocq.Erasure.Typed.Optimize]
trim_start [in MetaRocq.Erasure.Typed.Optimize]
trivial_hyp [in MetaRocq.Examples.tauto]
try_remove_n_lambdas [in MetaRocq.Examples.add_constructor]
try_reduce [in MetaRocq.Template.Checker]
tsize [in MetaRocq.Examples.tauto]
tsl_constructor_body [in MetaRocq.Examples.add_constructor]
TTconv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
TTconv [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
TTwf_local [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
TTwf_local [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
TTy_wf_local [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
tybranches [in MetaRocq.PCUIC.Bidirectional.BDTyping]
tybranches [in MetaRocq.PCUIC.PCUICTyping]
typechecking [in MetaRocq.Template.Checker]
typecheck_program [in MetaRocq.SafeChecker.PCUICSafeChecker]
typecheck_program [in MetaRocq.Template.Checker]
typed_erase_transform [in MetaRocq.ErasurePlugin.ETransform]
typed_erasure_pre [in MetaRocq.ErasurePlugin.ETransform]
typed_erase_and_print_template_program [in MetaRocq.ErasurePlugin.Erasure]
typed_erasure_config [in MetaRocq.ErasurePlugin.Erasure]
typed_erasure_pipeline [in MetaRocq.ErasurePlugin.Erasure]
typed_erase_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
TypeInstance [in MetaRocq.Template.TemplateMonad.Core]
TypeInstance [in MetaRocq.Template.TemplateMonad.Extractable]
TypeInstanceOptimized [in MetaRocq.Template.TemplateMonad.Core]
TypeInstanceUnoptimized [in MetaRocq.Template.TemplateMonad.Core]
type_var_info_of_flag [in MetaRocq.Erasure.Typed.Erasure]
type_of_constructor [in MetaRocq.PCUIC.PCUICTyping]
type_of_impl [in MetaRocq.Erasure.Typed.TypeAnnotations]
type_flag_to_tRel_kind [in MetaRocq.Erasure.Typed.TypeAnnotations]
type_error_sind [in MetaRocq.SafeChecker.PCUICErrors]
type_error_rec [in MetaRocq.SafeChecker.PCUICErrors]
type_error_ind [in MetaRocq.SafeChecker.PCUICErrors]
type_error_rect [in MetaRocq.SafeChecker.PCUICErrors]
type_of_subtype [in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_of_typing [in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_of [in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_of_constructor [in MetaRocq.Template.Typing]
type_error_sind [in MetaRocq.Template.Checker]
type_error_rec [in MetaRocq.Template.Checker]
type_error_ind [in MetaRocq.Template.Checker]
type_error_rect [in MetaRocq.Template.Checker]
typing_sum_size [in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_sind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_rec [in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_ind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_rect [in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_spine_sind [in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_rec [in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_ind [in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_rect [in MetaRocq.PCUIC.PCUICGeneration]
typing_size [in MetaRocq.PCUIC.PCUICTyping]
typing_sind [in MetaRocq.PCUIC.PCUICTyping]
typing_rec [in MetaRocq.PCUIC.PCUICTyping]
typing_ind [in MetaRocq.PCUIC.PCUICTyping]
typing_rect [in MetaRocq.PCUIC.PCUICTyping]
typing_error_forget [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_sind [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_rec [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_ind [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_rect [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_sind [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_rec [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_ind [in MetaRocq.SafeChecker.PCUICErrors]
typing_result_rect [in MetaRocq.SafeChecker.PCUICErrors]
typing_spine_sind [in MetaRocq.PCUIC.PCUICArities]
typing_spine_rec [in MetaRocq.PCUIC.PCUICArities]
typing_spine_ind [in MetaRocq.PCUIC.PCUICArities]
typing_spine_rect [in MetaRocq.PCUIC.PCUICArities]
typing_spine_pred_sind [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_rec [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_ind [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_rect [in MetaRocq.PCUIC.PCUICProgress]
typing_size [in MetaRocq.Template.Typing]
typing_spine_size [in MetaRocq.Template.Typing]
typing_spine_sind [in MetaRocq.Template.Typing]
typing_spine_rec [in MetaRocq.Template.Typing]
typing_spine_ind [in MetaRocq.Template.Typing]
typing_spine_rect [in MetaRocq.Template.Typing]
typing_sind [in MetaRocq.Template.Typing]
typing_rec [in MetaRocq.Template.Typing]
typing_ind [in MetaRocq.Template.Typing]
typing_rect [in MetaRocq.Template.Typing]
typing_result_sind [in MetaRocq.Template.Checker]
typing_result_rec [in MetaRocq.Template.Checker]
typing_result_ind [in MetaRocq.Template.Checker]
typing_result_rect [in MetaRocq.Template.Checker]
typing_spine_size [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_sind [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_rec [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_ind [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_rect [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
T_sind [in MetaRocq.Examples.demo]
T_rec [in MetaRocq.Examples.demo]
T_ind [in MetaRocq.Examples.demo]
T_rect [in MetaRocq.Examples.demo]
| 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) |