| 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 (definition)
T [in MetaCoq.Translations.standard_model]T [in MetaCoq.Translations.param_original]
tAnd [in MetaCoq.Examples.tauto]
target_wcbv_flags [in MetaCoq.Erasure.EWcbvEval]
tauto_s [in MetaCoq.Examples.tauto]
tauto_proc [in MetaCoq.Examples.tauto]
tCaseBrsProp [in MetaCoq.Template.Ast]
tCaseBrsProp [in MetaCoq.PCUIC.PCUICAst]
tCaseBrsProp_k [in MetaCoq.PCUIC.PCUICAst]
tCaseBrsType [in MetaCoq.Template.AstUtils]
tCasePredProp [in MetaCoq.Template.Ast]
tCasePredProp [in MetaCoq.PCUIC.PCUICAst]
tCasePredProp_k [in MetaCoq.PCUIC.PCUICAst]
tDummy [in MetaCoq.PCUIC.utils.PCUICOnOne]
tDummy [in MetaCoq.Template.Ast]
telescope [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
TemplateConversionPar.cumul_gen [in MetaCoq.Template.Typing]
TemplateTermUtils.destArity [in MetaCoq.Template.Ast]
TemplateTermUtils.inds [in MetaCoq.Template.Ast]
TemplateTerm.closedn [in MetaCoq.Template.Ast]
TemplateTerm.lift [in MetaCoq.Template.Ast]
TemplateTerm.mkApps [in MetaCoq.Template.Ast]
TemplateTerm.noccur_between [in MetaCoq.Template.Ast]
TemplateTerm.subst [in MetaCoq.Template.Ast]
TemplateTerm.subst_instance_constr [in MetaCoq.Template.Ast]
TemplateTerm.term [in MetaCoq.Template.Ast]
TemplateTerm.tInd [in MetaCoq.Template.Ast]
TemplateTerm.tLambda [in MetaCoq.Template.Ast]
TemplateTerm.tLetIn [in MetaCoq.Template.Ast]
TemplateTerm.tProd [in MetaCoq.Template.Ast]
TemplateTerm.tProj [in MetaCoq.Template.Ast]
TemplateTerm.tRel [in MetaCoq.Template.Ast]
TemplateTerm.tSort [in MetaCoq.Template.Ast]
TemplateTyping.infer_sorting [in MetaCoq.Template.Typing]
TemplateTyping.typing [in MetaCoq.Template.Typing]
template_to_pcuic_transform [in MetaCoq.PCUIC.PCUICTransform]
template_to_pcuic_obseq [in MetaCoq.PCUIC.PCUICTransform]
template_program [in MetaCoq.Template.TemplateProgram]
TermSpineView.view [in MetaCoq.Erasure.ESpineView]
term_flags [in MetaCoq.Erasure.EConstructorsAsBlocks]
term_subterm_wf [in MetaCoq.SafeChecker.PCUICWfReduction]
term_subterm_context [in MetaCoq.SafeChecker.PCUICWfReduction]
term_subterm [in MetaCoq.SafeChecker.PCUICWfReduction]
term_direct_subterm_context [in MetaCoq.SafeChecker.PCUICWfReduction]
term_rel [in MetaCoq.Erasure.ErasureFunction]
term_global_deps [in MetaCoq.Erasure.EAstUtils]
test [in MetaCoq.Examples.metacoq_tour]
test [in MetaCoq.Examples.add_constructor]
test_context_k [in MetaCoq.Template.BasicAst]
test_context [in MetaCoq.Template.BasicAst]
test_decl [in MetaCoq.Template.BasicAst]
test_def [in MetaCoq.Template.BasicAst]
test_branch [in MetaCoq.Template.Ast]
test_predicate_k [in MetaCoq.Template.Ast]
test_predicate [in MetaCoq.Template.Ast]
test_branch_k_pars [in MetaCoq.PCUIC.Syntax.PCUICPosition]
test_branches_nlict [in MetaCoq.PCUIC.PCUICAst]
test_branch_nlict [in MetaCoq.PCUIC.PCUICAst]
test_context_nlict [in MetaCoq.PCUIC.PCUICAst]
test_branch_k [in MetaCoq.PCUIC.PCUICAst]
test_branch [in MetaCoq.PCUIC.PCUICAst]
test_predicate_ku [in MetaCoq.PCUIC.PCUICAst]
test_predicate_k [in MetaCoq.PCUIC.PCUICAst]
test_predicate [in MetaCoq.PCUIC.PCUICAst]
test_def [in MetaCoq.Erasure.EAst]
test_snd [in MetaCoq.Template.utils.MCProd]
test' [in MetaCoq.Examples.add_constructor]
test2 [in MetaCoq.Examples.add_constructor]
test3 [in MetaCoq.Examples.add_constructor]
test4 [in MetaCoq.Examples.add_constructor]
tFixProp [in MetaCoq.Template.BasicAst]
tFixType [in MetaCoq.Template.AstUtils]
time [in MetaCoq.Template.Transform]
timesBool [in MetaCoq.Translations.times_bool_fun]
tImpl [in MetaCoq.Examples.typing_correctness]
tImpl [in MetaCoq.Examples.tauto]
tImpl [in MetaCoq.Examples.metacoq_tour_prelude]
Tlift_typing [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
tm [in MetaCoq.Translations.standard_model]
tm [in MetaCoq.Translations.param_original]
tmAxiom [in MetaCoq.Template.TemplateMonad.Core]
tmAxiomRed [in MetaCoq.Template.TemplateMonad.Extractable]
tmDebug [in MetaCoq.Translations.translation_utils]
tmDefinition [in MetaCoq.Template.TemplateMonad.Core]
tmDefinition [in MetaCoq.Template.TemplateMonad.Extractable]
tmDefinitionRed [in MetaCoq.Template.TemplateMonad.Core]
tmDefinitionRed [in MetaCoq.Template.TemplateMonad.Extractable]
tmInductive' [in MetaCoq.Template.TemplateMonad.Extractable]
tmInferInstanceRed [in MetaCoq.Template.TemplateMonad.Extractable]
tmLemmaRed [in MetaCoq.Template.TemplateMonad.Extractable]
tmLocateCst [in MetaCoq.Translations.translation_utils]
tmLocateInd [in MetaCoq.Examples.tauto]
tmLocate1 [in MetaCoq.Template.TemplateMonad.Core]
tmMkDefinition [in MetaCoq.Template.TemplateMonad.Core]
tmMkInductive' [in MetaCoq.Template.TemplateMonad.Core]
tmOpaqueDefinition [in MetaCoq.Template.TemplateMonad.Extractable]
tmOpaqueDefinitionRed [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteDefinition [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteDefinitionRed [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteRec [in MetaCoq.Template.TemplateMonad.Core]
tmQuoteRecDefinition [in MetaCoq.Template.TemplateMonad.Core]
tmTestQuote [in MetaCoq.Template.TemplateMonad.Core]
tmTestUnquote [in MetaCoq.Template.TemplateMonad.Core]
to [in MetaCoq.Translations.param_cheap_packed]
tOr [in MetaCoq.Examples.tauto]
toto [in MetaCoq.Translations.standard_model]
trans [in MetaCoq.PCUIC.PCUICExpandLets]
trans [in MetaCoq.PCUIC.TemplateToPCUIC]
trans [in MetaCoq.PCUIC.PCUICToTemplate]
transform_blocks_program [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_env [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_decl [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_constant_decl [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks [in MetaCoq.Erasure.EConstructorsAsBlocks]
Transform.compose [in MetaCoq.Template.Transform]
Transform.preserves_eval [in MetaCoq.Template.Transform]
Transform.run [in MetaCoq.Template.Transform]
Transform.self_transform [in MetaCoq.Template.Transform]
Translate [in MetaCoq.Translations.translation_utils]
TranslateRec [in MetaCoq.Translations.translation_utils]
TransLookup.lookup_inductive [in MetaCoq.PCUIC.PCUICProgram]
TransLookup.lookup_minductive [in MetaCoq.PCUIC.PCUICProgram]
transport [in MetaCoq.Template.utils.MCEquality]
transport [in MetaCoq.Translations.MiniHoTT]
transport [in MetaCoq.Translations.MiniHoTT_paths]
transportD [in MetaCoq.Translations.MiniHoTT]
transportD [in MetaCoq.Translations.MiniHoTT_paths]
transportD_is_transport [in MetaCoq.Translations.MiniHoTT]
transportD_is_transport [in MetaCoq.Translations.MiniHoTT_paths]
transportD2 [in MetaCoq.Translations.MiniHoTT]
transportD2 [in MetaCoq.Translations.MiniHoTT_paths]
transport_ws_term [in MetaCoq.PCUIC.PCUICConfluence]
transport_on_free_vars [in MetaCoq.PCUIC.PCUICConfluence]
transport_sigma_' [in MetaCoq.Translations.MiniHoTT]
transport_sigma' [in MetaCoq.Translations.MiniHoTT]
transport_sigma [in MetaCoq.Translations.MiniHoTT]
transport_pr1_path_sigma [in MetaCoq.Translations.MiniHoTT]
transport_forall_constant [in MetaCoq.Translations.MiniHoTT]
transport_forall [in MetaCoq.Translations.MiniHoTT]
transport_paths2 [in MetaCoq.Translations.MiniHoTT]
transport_paths_lFFr [in MetaCoq.Translations.MiniHoTT]
transport_paths_FFlr [in MetaCoq.Translations.MiniHoTT]
transport_paths_FlFr_D [in MetaCoq.Translations.MiniHoTT]
transport_paths_FlFr [in MetaCoq.Translations.MiniHoTT]
transport_paths_Fr [in MetaCoq.Translations.MiniHoTT]
transport_paths_Fl [in MetaCoq.Translations.MiniHoTT]
transport_paths_lr [in MetaCoq.Translations.MiniHoTT]
transport_paths_r [in MetaCoq.Translations.MiniHoTT]
transport_paths_l [in MetaCoq.Translations.MiniHoTT]
transport_transport [in MetaCoq.Translations.MiniHoTT]
transport_idmap_ap [in MetaCoq.Translations.MiniHoTT]
transport_const [in MetaCoq.Translations.MiniHoTT]
transport_pV_ap [in MetaCoq.Translations.MiniHoTT]
transport_VpV [in MetaCoq.Translations.MiniHoTT]
transport_pVp [in MetaCoq.Translations.MiniHoTT]
transport_p_pp [in MetaCoq.Translations.MiniHoTT]
transport_Vp [in MetaCoq.Translations.MiniHoTT]
transport_pV [in MetaCoq.Translations.MiniHoTT]
transport_pp [in MetaCoq.Translations.MiniHoTT]
transport_1 [in MetaCoq.Translations.MiniHoTT]
transport_beta [in MetaCoq.Translations.MiniHoTT]
transport_sigma_' [in MetaCoq.Translations.MiniHoTT_paths]
transport_sigma' [in MetaCoq.Translations.MiniHoTT_paths]
transport_sigma [in MetaCoq.Translations.MiniHoTT_paths]
transport_pr1_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
transport_forall_constant [in MetaCoq.Translations.MiniHoTT_paths]
transport_forall [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths2 [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_lFFr [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_FFlr [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_FlFr_D [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_FlFr [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_Fr [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_Fl [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_lr [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_r [in MetaCoq.Translations.MiniHoTT_paths]
transport_paths_l [in MetaCoq.Translations.MiniHoTT_paths]
transport_transport [in MetaCoq.Translations.MiniHoTT_paths]
transport_idmap_ap [in MetaCoq.Translations.MiniHoTT_paths]
transport_const [in MetaCoq.Translations.MiniHoTT_paths]
transport_pV_ap [in MetaCoq.Translations.MiniHoTT_paths]
transport_VpV [in MetaCoq.Translations.MiniHoTT_paths]
transport_pVp [in MetaCoq.Translations.MiniHoTT_paths]
transport_p_pp [in MetaCoq.Translations.MiniHoTT_paths]
transport_Vp [in MetaCoq.Translations.MiniHoTT_paths]
transport_pV [in MetaCoq.Translations.MiniHoTT_paths]
transport_pp [in MetaCoq.Translations.MiniHoTT_paths]
transport_1 [in MetaCoq.Translations.MiniHoTT_paths]
transport_beta [in MetaCoq.Translations.MiniHoTT_paths]
transport_Vp [in MetaCoq.Translations.times_bool_fun2]
transport_pV [in MetaCoq.Translations.times_bool_fun2]
transport2 [in MetaCoq.Translations.MiniHoTT]
transport2 [in MetaCoq.Translations.MiniHoTT_paths]
transport2_const [in MetaCoq.Translations.MiniHoTT]
transport2_V [in MetaCoq.Translations.MiniHoTT]
transport2_p2p [in MetaCoq.Translations.MiniHoTT]
transport2_is_ap10 [in MetaCoq.Translations.MiniHoTT]
transport2_const [in MetaCoq.Translations.MiniHoTT_paths]
transport2_V [in MetaCoq.Translations.MiniHoTT_paths]
transport2_p2p [in MetaCoq.Translations.MiniHoTT_paths]
transport2_is_ap10 [in MetaCoq.Translations.MiniHoTT_paths]
trans_def [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_global [in MetaCoq.PCUIC.PCUICExpandLets]
trans_global_env [in MetaCoq.PCUIC.PCUICExpandLets]
trans_global_decls [in MetaCoq.PCUIC.PCUICExpandLets]
trans_global_decl [in MetaCoq.PCUIC.PCUICExpandLets]
trans_constant_body [in MetaCoq.PCUIC.PCUICExpandLets]
trans_minductive_body [in MetaCoq.PCUIC.PCUICExpandLets]
trans_one_ind_body [in MetaCoq.PCUIC.PCUICExpandLets]
trans_projection_body [in MetaCoq.PCUIC.PCUICExpandLets]
trans_constructor_body [in MetaCoq.PCUIC.PCUICExpandLets]
trans_cstr_concl [in MetaCoq.PCUIC.PCUICExpandLets]
trans_cstr_concl_head [in MetaCoq.PCUIC.PCUICExpandLets]
trans_local [in MetaCoq.PCUIC.PCUICExpandLets]
trans_branch [in MetaCoq.PCUIC.PCUICExpandLets]
trans_def [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_template_program [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_global [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_global_env [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_global_decls [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_global_decl [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_minductive_body [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_constant_body [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_one_ind_body [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_projection_body [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_constructor_body [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_local [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_decl [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_branch [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_predicate [in MetaCoq.PCUIC.TemplateToPCUIC]
trans_program [in MetaCoq.SafeChecker.SafeTemplateChecker]
trans_global [in MetaCoq.PCUIC.PCUICToTemplate]
trans_global_env [in MetaCoq.PCUIC.PCUICToTemplate]
trans_global_decls [in MetaCoq.PCUIC.PCUICToTemplate]
trans_global_decl [in MetaCoq.PCUIC.PCUICToTemplate]
trans_minductive_body [in MetaCoq.PCUIC.PCUICToTemplate]
trans_constant_body [in MetaCoq.PCUIC.PCUICToTemplate]
trans_one_ind_body [in MetaCoq.PCUIC.PCUICToTemplate]
trans_projection_body [in MetaCoq.PCUIC.PCUICToTemplate]
trans_constructor_body [in MetaCoq.PCUIC.PCUICToTemplate]
trans_local [in MetaCoq.PCUIC.PCUICToTemplate]
trans_branch [in MetaCoq.PCUIC.PCUICToTemplate]
trans_predicate [in MetaCoq.PCUIC.PCUICToTemplate]
Tree.concat [in MetaCoq.Template.utils.bytestring]
Tree.parens [in MetaCoq.Template.utils.bytestring]
Tree.print_list [in MetaCoq.Template.utils.bytestring]
Tree.string_of_list [in MetaCoq.Template.utils.bytestring]
Tree.string_of_list_aux [in MetaCoq.Template.utils.bytestring]
Tree.to_string [in MetaCoq.Template.utils.bytestring]
Tree.to_string_acc [in MetaCoq.Template.utils.bytestring]
Tree.to_rev_list_aux [in MetaCoq.Template.utils.bytestring]
triangulator [in MetaCoq.Translations.MiniHoTT]
triangulator [in MetaCoq.Translations.MiniHoTT_paths]
trivial_hyp [in MetaCoq.Examples.tauto]
try_reduce [in MetaCoq.Template.Checker]
try_remove_n_lambdas [in MetaCoq.Examples.add_constructor]
tsize [in MetaCoq.Examples.tauto]
tsl [in MetaCoq.Translations.standard_model]
tsl_name [in MetaCoq.Translations.translation_utils]
tsl_name0 [in MetaCoq.Translations.translation_utils]
tsl_ident [in MetaCoq.Translations.translation_utils]
tsl_context [in MetaCoq.Translations.translation_utils]
tsl_table [in MetaCoq.Translations.translation_utils]
tsl_mind_body [in MetaCoq.Translations.param_binary]
tsl_rec1 [in MetaCoq.Translations.param_binary]
tsl_rec1_app [in MetaCoq.Translations.param_binary]
tsl_rec0 [in MetaCoq.Translations.param_binary]
tsl_mind_body [in MetaCoq.Translations.times_bool_fun]
tsl_rec [in MetaCoq.Translations.times_bool_fun]
tsl_mind_body [in MetaCoq.Translations.param_cheap_packed]
tsl_term [in MetaCoq.Translations.param_cheap_packed]
tsl_rec2 [in MetaCoq.Translations.param_cheap_packed]
tsl_rec1 [in MetaCoq.Translations.param_cheap_packed]
tsl_ctx [in MetaCoq.Translations.standard_model]
tsl_mind_body [in MetaCoq.Translations.param_original]
tsl_rec1 [in MetaCoq.Translations.param_original]
tsl_rec1_app [in MetaCoq.Translations.param_original]
tsl_rec0 [in MetaCoq.Translations.param_original]
tsl_term [in MetaCoq.Translations.param_generous_packed]
tsl_rec [in MetaCoq.Translations.param_generous_packed]
tsl_constructor_body [in MetaCoq.Examples.add_constructor]
TTconv [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
TTconv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
TTwf_local [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
TTwf_local [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
TTy_wf_local [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ty [in MetaCoq.Translations.param_cheap_packed]
Ty [in MetaCoq.Translations.param_generous_packed]
tybranches [in MetaCoq.PCUIC.Bidirectional.BDTyping]
tybranches [in MetaCoq.PCUIC.PCUICTyping]
typechecking [in MetaCoq.Template.Checker]
typecheck_program [in MetaCoq.Template.Checker]
typecheck_program [in MetaCoq.SafeChecker.PCUICSafeChecker]
TypeInstance [in MetaCoq.Template.TemplateMonad.Extractable]
type_of_constructor [in MetaCoq.Template.Typing]
type_of_subtype [in MetaCoq.SafeChecker.PCUICSafeRetyping]
type_of_typing [in MetaCoq.SafeChecker.PCUICSafeRetyping]
type_of [in MetaCoq.SafeChecker.PCUICSafeRetyping]
type_of_constructor [in MetaCoq.PCUIC.PCUICTyping]
typing_sum_size [in MetaCoq.PCUIC.Bidirectional.BDTyping]
typing_spine_size [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
typing_size [in MetaCoq.Template.Typing]
typing_spine_size [in MetaCoq.Template.Typing]
typing_error_forget [in MetaCoq.SafeChecker.PCUICErrors]
typing_size [in MetaCoq.PCUIC.PCUICTyping]
typ_or_sort_default [in MetaCoq.Template.BasicAst]
typ_or_sort_map [in MetaCoq.Template.BasicAst]
| 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) |