| 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) |
D
d [definition, in MetaRocq.Examples.demo]dapp_r [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dapp_l [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dbody [projection, in MetaRocq.Common.BasicAst]
dbody [projection, in MetaRocq.Erasure.EAst]
dcase_c [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dcase_preturn [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dearg [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg [section, in MetaRocq.Erasure.Typed.Optimize]
dearg [definition, in MetaRocq.ErasurePlugin.ETransform]
dearg [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearged_proj_arg [definition, in MetaRocq.Erasure.Typed.Optimize]
dearged_npars [definition, in MetaRocq.Erasure.Typed.Optimize]
dearged_ctor_arity [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Dearging [section, in MetaRocq.ErasurePlugin.ETransform]
dearging_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
dearging_checks_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
dearging_config [record, in MetaRocq.ErasurePlugin.ETransform]
dearging_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
dearging_checks_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
dearging_config [projection, in MetaRocq.ErasurePlugin.Erasure]
dearg_transform [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_set [record, in MetaRocq.Erasure.Typed.Optimize]
dearg_single_bt [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_types.Σ [variable, in MetaRocq.Erasure.Typed.Optimize]
dearg_types [section, in MetaRocq.Erasure.Typed.Optimize]
dearg_env [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_decl [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_mib [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_oib [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_ctor [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_cst [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_cst_type_top [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_aux [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_proj [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_case [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_case_branches [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_case_branch [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_branch_body [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_branch_body_rec_count_zeros [lemma, in MetaRocq.Erasure.Typed.Optimize]
dearg_branch_body_rec [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_lambdas [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_single [definition, in MetaRocq.Erasure.Typed.Optimize]
dearg_transform_correct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_transform_gen_correct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_term [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_env [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_repeat_tBox [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_substl_correct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_all_zeros [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.EtaFix [section, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.IH [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.exp_Σ [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.valid_Σ [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.clos_Σ [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.Σ [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.n [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg.wfl [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.dearg [section, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_cunfold_cofix [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_cunfold_fix [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_substl [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_elim [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_sind [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_rec [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_ind [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_rect [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_other [constructor, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_proj [constructor, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_case [constructor, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_ctor [constructor, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_const [constructor, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec [inductive, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_aux_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_expanded [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_expanded_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_single_enough_args [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_lift [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_aux_mkApps [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_proj [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_case [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_cst [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_decl [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_env [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_aux [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.const_masks [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct.ind_masks [variable, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct [section, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_correct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_single_masked [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_nil [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg.const_masks [variable, in MetaRocq.Erasure.Typed.Optimize]
dearg.ind_masks [variable, in MetaRocq.Erasure.Typed.Optimize]
debox_env_types [definition, in MetaRocq.Erasure.Typed.Optimize]
debox_type_decl [definition, in MetaRocq.Erasure.Typed.Optimize]
debox_type_mib [definition, in MetaRocq.Erasure.Typed.Optimize]
debox_type_oib [definition, in MetaRocq.Erasure.Typed.Optimize]
debox_type_constant [definition, in MetaRocq.Erasure.Typed.Optimize]
debox_box_type [definition, in MetaRocq.Erasure.Typed.Optimize]
debox_box_type_aux [definition, in MetaRocq.Erasure.Typed.Optimize]
debug [projection, in MetaRocq.Quotation.CommonUtils]
debug [constructor, in MetaRocq.Quotation.CommonUtils]
debug_opt [record, in MetaRocq.Quotation.CommonUtils]
debug_opt [inductive, in MetaRocq.Quotation.CommonUtils]
decision [abbreviation, in MetaRocq.PCUIC.PCUICNormal]
DeclarationTyping [module, in MetaRocq.Common.EnvironmentTyping]
DeclarationTypingSig [module, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_projection_from_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_projection_to_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constructor_from_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constructor_to_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_inductive_from_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_inductive_to_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_minductive_from_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_minductive_to_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constant_to_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constant_from_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.Forall_decls_typing [definition, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.isType [definition, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.on_wf_global_env_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.on_wf_global_env_impl_config [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.Properties [section, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.Properties.cf [variable, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.Properties.P [variable, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.Properties.Pcmp [variable, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.Properties.wf [variable, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.refine_type [lemma, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.type_local_decl [definition, in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.wf_local_rel [definition, in MetaRocq.Common.EnvironmentTyping]
declared [definition, in MetaRocq.Common.uGraph]
DeclaredInv [section, in MetaRocq.PCUIC.PCUICGlobalEnv]
DeclaredInv.cf [variable, in MetaRocq.PCUIC.PCUICGlobalEnv]
DeclaredInv.wfΣ [variable, in MetaRocq.PCUIC.PCUICGlobalEnv]
DeclaredInv.Σ [variable, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_minductive_closed_inds [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
declared_projection_indices [lemma, in MetaRocq.PCUIC.PCUICSR]
declared_projection_declared_constructor [lemma, in MetaRocq.PCUIC.PCUICSR]
declared_constructor_assumption_context [lemma, in MetaRocq.Erasure.Prelim]
declared_projection_projs_nonempty [lemma, in MetaRocq.PCUIC.PCUICElimination]
declared_constructor_arity [lemma, in MetaRocq.Erasure.ErasureCorrectness]
declared_cstr_levels [definition, in MetaRocq.Common.Universes]
declared_cstr_levels_sub [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
declared_minductive_ind_npars [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_projection_constructor' [definition, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_projection_constructor [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constructor_inductive' [definition, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constructor_inductive [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_minductive' [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_minductive [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_projection_inj [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constructor_inj [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_inj [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constant_inj [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_kn [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
declared_inductive_closed_indices [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
declared_inductive_unique_sig [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
declared_inductive_unique [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
declared_constructor_valid_ty [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
declared_constructor_ind_decl [lemma, in MetaRocq.PCUIC.PCUICProgress]
declared_projection_type_and_eq [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_projection_type [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_projections_subslet [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_projections [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_projections_subslet_ind [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_constructor_wf_pars_args [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_inductive_valid_type [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_inductive_type [lemma, in MetaRocq.PCUIC.PCUICInductives]
declared_constant_All [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
declared_constant_Forall [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
declared_constructor_wf_case_branch_context [lemma, in MetaRocq.Template.TypingWf]
declared_inductive_wf_case_predicate_context [lemma, in MetaRocq.Template.TypingWf]
declared_minductive_wf [lemma, in MetaRocq.Template.TypingWf]
declared_constant_wf [lemma, in MetaRocq.Template.TypingWf]
declared_projection_wf [lemma, in MetaRocq.Template.TypingWf]
declared_constructor_wf [lemma, in MetaRocq.Template.TypingWf]
declared_inductive_wf_params [lemma, in MetaRocq.Template.TypingWf]
declared_inductive_wf_ctors [lemma, in MetaRocq.Template.TypingWf]
declared_inductive_wf_indices [lemma, in MetaRocq.Template.TypingWf]
declared_inductive_wf [lemma, in MetaRocq.Template.TypingWf]
declared_env_extends [lemma, in MetaRocq.Template.TypingWf]
declared_inductive_wf_global_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
declared_inductive_wf_ext_wk [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
declared_constructor_typing_spine_not_arity [lemma, in MetaRocq.Erasure.EArities]
declared_constructor_type_not_arity [lemma, in MetaRocq.Erasure.EArities]
declared_constant_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
declared_constant_trans_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
declared_global_uctx_global_ext_uctx [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
declared_projection_lookup [lemma, in MetaRocq.Erasure.EGlobalEnv]
declared_constructor_lookup [lemma, in MetaRocq.Erasure.EGlobalEnv]
declared_inductive_lookup [lemma, in MetaRocq.Erasure.EGlobalEnv]
declared_minductive_lookup [lemma, in MetaRocq.Erasure.EGlobalEnv]
declared_constant_lookup [lemma, in MetaRocq.Erasure.EGlobalEnv]
declared_projection [definition, in MetaRocq.Erasure.EGlobalEnv]
declared_constructor [definition, in MetaRocq.Erasure.EGlobalEnv]
declared_inductive [definition, in MetaRocq.Erasure.EGlobalEnv]
declared_minductive [definition, in MetaRocq.Erasure.EGlobalEnv]
declared_constant [definition, in MetaRocq.Erasure.EGlobalEnv]
declared_projection_unique [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
declared_constructor_unique [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
declared_inductive_lookup [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
declared_inductive_inj [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
declared_projection_closed_type [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_indices [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_args [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_type [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_gen_type [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed_arities [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_constructors [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_params_inst [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_params [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_type [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constant_closed_body [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constant_closed_type [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_decl_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_pars_indices [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_projection_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed_ind [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_decl_closed_ind [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_projection_closed_ind [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_expanded [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
declared_minductive_expanded [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
declared_projection_inv [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_inv_decls [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_inductive_inv_decls [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_minductive_inv_decls [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_inv [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_inductive_inv [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_minductive_inv [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constant_inv [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declare_and_uniquify_and_combine_levels [definition, in MetaRocq.Common.UniversesDec]
declare_and_uniquify_levels [definition, in MetaRocq.Common.UniversesDec]
decls_prefix_wf [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
decls_prefix [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
decl_deps [definition, in MetaRocq.Erasure.Typed.Erasure]
decl_hole_body [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decl_hole_type [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decl_size [definition, in MetaRocq.Examples.tauto]
decl_closed [definition, in MetaRocq.Erasure.Typed.ClosedAux]
decl_type_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
decl_body_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
decl_ws_cumul_pb [abbreviation, in MetaRocq.PCUIC.PCUICInductiveInversion]
decl_size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
decl_size_map_decl_hom [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
decl_type [projection, in MetaRocq.Common.BasicAst]
decl_body [projection, in MetaRocq.Common.BasicAst]
decl_name [projection, in MetaRocq.Common.BasicAst]
decl_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
decl_body [projection, in MetaRocq.Erasure.EAst]
decl_name [projection, in MetaRocq.Erasure.EAst]
decompose_prod_n_assum_extend_ctx [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
decompose_stack_twice [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_appstack [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_not_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_app_rec_inv2 [lemma, in MetaRocq.Erasure.Prelim]
decompose_app_wf [lemma, in MetaRocq.Examples.tauto]
decompose_app_eq [lemma, in MetaRocq.Examples.tauto]
decompose_stack_at_appstack_None [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
decompose_prod_assum_spec [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_sind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_rec [definition, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_ind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_rect [definition, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_arity [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph [inductive, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_n_assum0 [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_app_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_app_rec_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
decompose_lam [definition, in MetaRocq.Template.Pretty]
decompose_arr [definition, in MetaRocq.Erasure.Typed.ExAst]
decompose_stack_stack_cat [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
decompose_stack_noStackApp [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
decompose_stack_closed [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
decompose_prod_assum_it_mkProd [lemma, in MetaRocq.Template.AstUtils]
decompose_prod_n_assum_it_mkProd [lemma, in MetaRocq.Template.AstUtils]
decompose_lam_n_assum [definition, in MetaRocq.Template.AstUtils]
decompose_prod_n_assum [definition, in MetaRocq.Template.AstUtils]
decompose_prod_assum [definition, in MetaRocq.Template.AstUtils]
decompose_prod [definition, in MetaRocq.Template.AstUtils]
decompose_app_mkApps [lemma, in MetaRocq.Template.AstUtils]
decompose_app [definition, in MetaRocq.Template.AstUtils]
decompose_app_tApp_split [lemma, in MetaRocq.Erasure.EUnboxing]
decompose_TArr [definition, in MetaRocq.Erasure.Typed.Optimize]
decompose_app_rec_inv' [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_eq [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_eq_right [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_tFix [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_tFix [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_head [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_eq_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_nonnil [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_inv [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_inv [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_notApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_notApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum_it_mkProd [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_n_assum_it_mkProd [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_n_assum [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum_ctx [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_type_of_constructor [lemma, in MetaRocq.Template.EtaExpand]
decompose_prod12 [lemma, in MetaRocq.Template.EtaExpand]
decompose_prod_lift [lemma, in MetaRocq.Template.EtaExpand]
decompose_lam [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
decompose_prod_assum_upto_names' [lemma, in MetaRocq.PCUIC.PCUICAlpha]
decompose_app_upto [lemma, in MetaRocq.PCUIC.PCUICAlpha]
decompose_app_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
decompose_app_rec_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
decompose_app_tApp_split [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
decompose_lam [definition, in MetaRocq.Erasure.Typed.CertifyingBeta]
decompose_app_size_tApp2 [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_app_size_tApp1 [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_app_rec_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_app_rec_length_mono [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_prod_n_assum_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
decompose_cstr_concl [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
decompose_prod_assum_it_mkProd_or_LetIn' [lemma, in MetaRocq.PCUIC.PCUICInductives]
decompose_app_inst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
decompose_app_rec_inst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
decompose_lam [definition, in MetaRocq.Erasure.EPretty]
decompose_app_inv [lemma, in MetaRocq.Template.TypingWf]
decompose_app_mkApp [lemma, in MetaRocq.Template.TypingWf]
decompose_body_masked_spec [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
decompose_body_masked [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
decompose_app_app [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_notApp [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_rec_notApp [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_inv [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_rec_inv [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_size [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_rec_size [lemma, in MetaRocq.Erasure.EInduction]
decompose_app_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
decompose_prod_assum_mkApps [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
decompose_app_tApp_split [lemma, in MetaRocq.Erasure.ERemoveParams]
decompose_prod_assum_it_mkProd_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
decompose_prod_assum_mkApps_nonnil [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
decompose_app_rec_inv' [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_eq [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_eq_right [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_notApp [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_notApp [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_inv [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_inv [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app_head_spine [lemma, in MetaRocq.Erasure.EAstUtils]
decompose_app [definition, in MetaRocq.Erasure.EAstUtils]
decompose_app_rec [definition, in MetaRocq.Erasure.EAstUtils]
decomp_step_size [lemma, in MetaRocq.Examples.tauto]
decomp_step [definition, in MetaRocq.Examples.tauto]
decomp_branch' [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
decomp_branch [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
dec_All [lemma, in MetaRocq.PCUIC.PCUICNormal]
dedup_grefs [definition, in MetaRocq.Quotation.CommonUtils]
dedup_grefs' [definition, in MetaRocq.Quotation.CommonUtils]
def [record, in MetaRocq.Common.BasicAst]
def [record, in MetaRocq.Erasure.EAst]
default_checker_flags [instance, in MetaRocq.Common.config]
default_relevance [definition, in MetaRocq.Template.AstUtils]
default_sort_family [definition, in MetaRocq.Template.AstUtils]
default_eval_pcuic_quotation [instance, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
default_inductive_quotation_of [definition, in MetaRocq.Quotation.ToPCUIC.Init]
default_normalizing [instance, in MetaRocq.PCUIC.PCUICSN]
default_inductive_quotation_of [definition, in MetaRocq.Quotation.ToTemplate.Init]
default_wcbv_flags [definition, in MetaRocq.Erasure.EWcbvEval]
default_erasure_config [definition, in MetaRocq.ErasurePlugin.Erasure]
default_unsafe_passes [definition, in MetaRocq.ErasurePlugin.Erasure]
default_dearging_config [definition, in MetaRocq.ErasurePlugin.Erasure]
default_fuel [definition, in MetaRocq.Template.Checker]
DefinitionEntry [constructor, in MetaRocq.PCUIC.PCUICAst]
DefinitionEntry [constructor, in MetaRocq.Erasure.EAst]
DefinitionEntry [constructor, in MetaRocq.Template.Ast]
definition_entry_opaque [projection, in MetaRocq.PCUIC.PCUICAst]
definition_entry_universes [projection, in MetaRocq.PCUIC.PCUICAst]
definition_entry_body [projection, in MetaRocq.PCUIC.PCUICAst]
definition_entry_type [projection, in MetaRocq.PCUIC.PCUICAst]
definition_entry [record, in MetaRocq.PCUIC.PCUICAst]
definition_entry_opaque [projection, in MetaRocq.Erasure.EAst]
definition_entry_body [projection, in MetaRocq.Erasure.EAst]
definition_entry [record, in MetaRocq.Erasure.EAst]
definition_entry_opaque [projection, in MetaRocq.Template.Ast]
definition_entry_universes [projection, in MetaRocq.Template.Ast]
definition_entry_body [projection, in MetaRocq.Template.Ast]
definition_entry_type [projection, in MetaRocq.Template.Ast]
definition_entry [record, in MetaRocq.Template.Ast]
def_sig [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
def_hole_body [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
def_hole_type [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
def_hole [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
def_size [definition, in MetaRocq.Examples.tauto]
def_size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
def_eq_dec [instance, in MetaRocq.Common.BasicAst]
def_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
demo [library]
depth [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_instance_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_decl [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
deriv_length_min [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
deriv_length [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
destArity [definition, in MetaRocq.PCUIC.PCUICAst]
destArity [definition, in MetaRocq.Template.Ast]
destArity_spec_Some [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
destArity_spec [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
destArity_mkApps_Ind [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_mkApps_None [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_tInd [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_tApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_tFix [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_app_Some [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_app [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_app_aux [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
destArity_it_mkProd_or_LetIn [lemma, in MetaRocq.Template.TypingWf]
destArity_spec [lemma, in MetaRocq.Template.TypingWf]
destArity_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
destInd [definition, in MetaRocq.Template.AstUtils]
destInd [definition, in MetaRocq.PCUIC.PCUICTyping]
destInd [definition, in MetaRocq.Template.Typing]
destInd_spec [lemma, in MetaRocq.PCUIC.PCUICAlpha]
destInd_Some_eq [lemma, in MetaRocq.PCUIC.PCUICInductives]
destInd_head_lift_inv [lemma, in MetaRocq.PCUIC.PCUICInductives]
destInd_head_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
destInd_head_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
destInd_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
DestructHead [library]
DestructHyps [library]
diamond [definition, in MetaRocq.PCUIC.PCUICConfluence]
diamond_pred1_rel_alpha [lemma, in MetaRocq.PCUIC.PCUICConfluence]
diamond_pred1_rel [lemma, in MetaRocq.PCUIC.PCUICConfluence]
diamond_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
diamond_t_t_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
diamond_t1n_t1n_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
diamond_t1n_t_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
diamond_proper [instance, in MetaRocq.PCUIC.PCUICConfluence]
dirpath [definition, in MetaRocq.Common.Kernames]
DirPathMap [module, in MetaRocq.Common.Kernames]
DirPathMapDecide [module, in MetaRocq.Common.Kernames]
DirPathMapExtraFact [module, in MetaRocq.Common.Kernames]
DirPathMapFact [module, in MetaRocq.Common.Kernames]
DirPathOT [module, in MetaRocq.Common.Kernames]
DirPathOTOrig [module, in MetaRocq.Common.Kernames]
DirPathSet [module, in MetaRocq.Common.Kernames]
DirPathSetDecide [module, in MetaRocq.Common.Kernames]
DirPathSetExtraDecide [module, in MetaRocq.Common.Kernames]
DirPathSetExtraOrdProp [module, in MetaRocq.Common.Kernames]
DirPathSetFact [module, in MetaRocq.Common.Kernames]
DirPathSetOrdProp [module, in MetaRocq.Common.Kernames]
DirPathSetProp [module, in MetaRocq.Common.Kernames]
dirpath_eqdec [instance, in MetaRocq.Common.Kernames]
disable_box_term_flags [definition, in MetaRocq.Erasure.EImplementBox]
disable_prop_cases [definition, in MetaRocq.Erasure.EWcbvEval]
disable_prop_cases [definition, in MetaRocq.Erasure.EInlineProjections]
disable_projections_env_flag [definition, in MetaRocq.Erasure.EInlineProjections]
disable_projections_term_flags [definition, in MetaRocq.Erasure.EInlineProjections]
Discharge [constructor, in MetaRocq.Template.TemplateMonad.Common]
discr_construct0_cofix [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
discr_construct_cofix [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
discr_construct [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
discr_construct [definition, in MetaRocq.Erasure.EEtaExpanded]
discr_expanded_head [definition, in MetaRocq.Erasure.EEtaExpandedFix]
discr_construct0_cofix [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
discr_construct_cofix [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
discr_prod_letin [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
DistinctCoFix [constructor, in MetaRocq.SafeChecker.PCUICErrors]
DistinctPrimTags [constructor, in MetaRocq.SafeChecker.PCUICErrors]
DistinctPrimValues [constructor, in MetaRocq.SafeChecker.PCUICErrors]
DistinctStuckProj [constructor, in MetaRocq.SafeChecker.PCUICErrors]
distr_lift_subst_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst10 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst_context_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
distr_subst [lemma, in MetaRocq.Template.LiftSubst]
distr_subst_rec [lemma, in MetaRocq.Template.LiftSubst]
distr_lift_subst10 [lemma, in MetaRocq.Template.LiftSubst]
distr_lift_subst [lemma, in MetaRocq.Template.LiftSubst]
distr_lift_subst_rec [lemma, in MetaRocq.Template.LiftSubst]
distr_subst [lemma, in MetaRocq.Erasure.ELiftSubst]
distr_subst_rec [lemma, in MetaRocq.Erasure.ELiftSubst]
distr_lift_subst10 [lemma, in MetaRocq.Erasure.ELiftSubst]
distr_lift_subst [lemma, in MetaRocq.Erasure.ELiftSubst]
distr_lift_subst_rec [lemma, in MetaRocq.Erasure.ELiftSubst]
dlam_tm [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlam_ty [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlet_in [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlet_ty [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlet_bd [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlexmod [inductive, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexmod_Acc [lemma, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexmod_sind [definition, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexmod_ind [definition, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod [inductive, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_Acc_gen [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
dlexprod_trans [instance, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_Acc [lemma, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_sind [definition, in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_ind [definition, in MetaRocq.PCUIC.utils.PCUICUtils]
dname [projection, in MetaRocq.Common.BasicAst]
dname [projection, in MetaRocq.Erasure.EAst]
do_eval_pcuic_quotation [instance, in MetaRocq.Quotation.ToPCUIC.Init]
do_check_ind_sorts [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
do_trim_ctor_masks [projection, in MetaRocq.ErasurePlugin.ETransform]
do_trim_const_masks [projection, in MetaRocq.ErasurePlugin.ETransform]
dprod_r [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dprod_l [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dproj_c [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
dtype [projection, in MetaRocq.Common.BasicAst]
dummy_branch [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
dummy_decl [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
dummy_branch [definition, in MetaRocq.Template.Typing]
dupfree [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
dupfree_dec_ident [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
| 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) |