| 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) |
O (lemma)
obseq_lambdabox [in MetaRocq.ErasurePlugin.ErasureCorrectness]obseq_compose_assoc [in MetaRocq.ErasurePlugin.ErasureCorrectness]
of_global_env_cons [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
of_global_env_cons [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
onctxP [in MetaRocq.Common.BasicAst]
onctx_eq_ctx_impl [in MetaRocq.PCUIC.PCUICEquality]
onctx_eq_ctx_trans [in MetaRocq.PCUIC.PCUICEquality]
onctx_eq_ctx_sym [in MetaRocq.PCUIC.PCUICEquality]
onctx_eq_ctx [in MetaRocq.PCUIC.PCUICEquality]
onctx_k_P [in MetaRocq.PCUIC.PCUICAst]
onctx_k_shift [in MetaRocq.PCUIC.PCUICAst]
onctx_k_rev [in MetaRocq.PCUIC.PCUICAst]
onctx_test [in MetaRocq.PCUIC.PCUICAst]
onctx_rel_pred1_refl' [in MetaRocq.PCUIC.PCUICParallelReduction]
onctx_rel_pred1_refl [in MetaRocq.PCUIC.PCUICParallelReduction]
onctx_fold_context_term [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
onctx_All_fold [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
ondeclP [in MetaRocq.Common.BasicAst]
ondecl_on_free_vars_decl [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
ondecl_map [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
one_inductive_body_eq [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
one_to_one_map_spec [in MetaRocq.Erasure.EReorderCstrs]
onfvs_app [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2All_All3 [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
OnOne2All_map2_map_all [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2All_All3 [in MetaRocq.Utils.All_Forall]
OnOne2All_nth_error_impl [in MetaRocq.Utils.All_Forall]
OnOne2All_impl_All_r [in MetaRocq.Utils.All_Forall]
OnOne2All_nth_error_r [in MetaRocq.Utils.All_Forall]
OnOne2All_nth_error [in MetaRocq.Utils.All_Forall]
OnOne2All_impl [in MetaRocq.Utils.All_Forall]
OnOne2All_split [in MetaRocq.Utils.All_Forall]
OnOne2All_impl_exist_and_All_r [in MetaRocq.Utils.All_Forall]
OnOne2All_impl_exist_and_All [in MetaRocq.Utils.All_Forall]
OnOne2All_ind_l [in MetaRocq.Utils.All_Forall]
OnOne2All_exist [in MetaRocq.Utils.All_Forall]
OnOne2All_sym [in MetaRocq.Utils.All_Forall]
OnOne2All_map_all [in MetaRocq.Utils.All_Forall]
OnOne2All_map [in MetaRocq.Utils.All_Forall]
OnOne2All_mapP [in MetaRocq.Utils.All_Forall]
OnOne2All_length2 [in MetaRocq.Utils.All_Forall]
OnOne2All_length [in MetaRocq.Utils.All_Forall]
OnOne2All_app [in MetaRocq.Utils.All_Forall]
OnOne2All_All2_mix_left [in MetaRocq.Utils.All_Forall]
OnOne2All_All_mix_left [in MetaRocq.Utils.All_Forall]
OnOne2All_on_Trel_eq_red_redl [in MetaRocq.PCUIC.PCUICReduction]
OnOne2All_red_redl [in MetaRocq.PCUIC.PCUICReduction]
OnOne2All_All2_All2 [in MetaRocq.Template.TypingWf]
OnOne2All_map2_map_all [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
OnOne2All_map2 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
OnOne2All2i_OnOne2All [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2All2i_OnOne2All [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
OnOne2i_nth_error_r [in MetaRocq.Utils.All_Forall]
OnOne2i_nth_error [in MetaRocq.Utils.All_Forall]
OnOne2i_impl [in MetaRocq.Utils.All_Forall]
OnOne2i_split [in MetaRocq.Utils.All_Forall]
OnOne2i_impl_exist_and_All_r [in MetaRocq.Utils.All_Forall]
OnOne2i_impl_exist_and_All [in MetaRocq.Utils.All_Forall]
OnOne2i_ind_l [in MetaRocq.Utils.All_Forall]
OnOne2i_exist [in MetaRocq.Utils.All_Forall]
OnOne2i_sym [in MetaRocq.Utils.All_Forall]
OnOne2i_map [in MetaRocq.Utils.All_Forall]
OnOne2i_mapP [in MetaRocq.Utils.All_Forall]
OnOne2i_length [in MetaRocq.Utils.All_Forall]
OnOne2i_app_r [in MetaRocq.Utils.All_Forall]
OnOne2i_app [in MetaRocq.Utils.All_Forall]
OnOne2i_All_mix_left [in MetaRocq.Utils.All_Forall]
OnOne2_nth_error [in MetaRocq.PCUIC.PCUICNormal]
OnOne2_local_env_forget_types [in MetaRocq.PCUIC.PCUICSR]
OnOne2_All2i_All2i [in MetaRocq.PCUIC.PCUICSR]
OnOne2_All2_All2 [in MetaRocq.PCUIC.PCUICSR]
OnOne2_ctx_inst [in MetaRocq.PCUIC.PCUICSpine]
OnOne2_local_env_impl_test [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_test_context_k [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_mapi_context [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_map_context [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_map [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_ondecl_impl [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_impl [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_pred1_ctx_over [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_pars_pred1_ctx_over [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_disj [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_All2_fold [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_exist' [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_exist' [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_apply_dep [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_apply [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_sigma [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_apply_All [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_apply [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_prod_assoc [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_prod [in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_All_All2 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_All_OnOne2 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_All2i_All2 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_local_env_All2_fold [in MetaRocq.PCUIC.PCUICContextReduction]
OnOne2_map_inv [in MetaRocq.Utils.All_Forall]
OnOne2_All_All [in MetaRocq.Utils.All_Forall]
OnOne2_All2_All2 [in MetaRocq.Utils.All_Forall]
OnOne2_impl_All_r [in MetaRocq.Utils.All_Forall]
OnOne2_nth_error_r [in MetaRocq.Utils.All_Forall]
OnOne2_nth_error [in MetaRocq.Utils.All_Forall]
OnOne2_impl [in MetaRocq.Utils.All_Forall]
OnOne2_split [in MetaRocq.Utils.All_Forall]
OnOne2_impl_exist_and_All_r [in MetaRocq.Utils.All_Forall]
OnOne2_impl_exist_and_All [in MetaRocq.Utils.All_Forall]
OnOne2_ind_l [in MetaRocq.Utils.All_Forall]
OnOne2_exist [in MetaRocq.Utils.All_Forall]
OnOne2_sym [in MetaRocq.Utils.All_Forall]
OnOne2_map [in MetaRocq.Utils.All_Forall]
OnOne2_mapP [in MetaRocq.Utils.All_Forall]
OnOne2_length [in MetaRocq.Utils.All_Forall]
OnOne2_app_r [in MetaRocq.Utils.All_Forall]
OnOne2_app [in MetaRocq.Utils.All_Forall]
OnOne2_All_mix_both [in MetaRocq.Utils.All_Forall]
OnOne2_All_mix_left [in MetaRocq.Utils.All_Forall]
OnOne2_All2 [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_prod_inv_refl_r [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_prod_inv [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_context_redl [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_on_Trel_eq_red_redl [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_on_Trel_eq_unit [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_red_redl [in MetaRocq.PCUIC.PCUICReduction]
OnOne2_All_All [in MetaRocq.Template.TypingWf]
OnOne2_map2 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
onPrims_map_prop [in MetaRocq.PCUIC.utils.PCUICPrimitive]
on_free_vars_type [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_branch_type [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_subst0 [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_subst [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_branch_context [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_predicate_context [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_ctx_tip [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_ctx_free_vars_strengthenP [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_rename [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICSR]
on_free_vars_ctx_tip [in MetaRocq.PCUIC.PCUICSR]
on_constructor_closed_indices_inst [in MetaRocq.PCUIC.PCUICSR]
on_free_vars_closedn [in MetaRocq.PCUIC.PCUICSR]
on_constructor_wf_arities_pars_args [in MetaRocq.PCUIC.PCUICSR]
on_constructor_closed_indices [in MetaRocq.PCUIC.PCUICSR]
on_free_vars_ctx_set_binder_name [in MetaRocq.PCUIC.PCUICSR]
on_constructor_wf_args [in MetaRocq.PCUIC.PCUICSR]
on_hyps_sound [in MetaRocq.Examples.tauto]
on_hyp_sound [in MetaRocq.Examples.tauto]
on_hyps_size [in MetaRocq.Examples.tauto]
on_hyp_size [in MetaRocq.Examples.tauto]
on_ctx_free_vars_snoc [in MetaRocq.PCUIC.PCUICSubstitution]
on_constructor_closed [in MetaRocq.PCUIC.PCUICSubstitution]
on_constructor_closed_arities [in MetaRocq.PCUIC.PCUICSubstitution]
on_free_vars_ctx_inst_case_context [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
on_free_vars_rename [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
on_minductive_wf_params_indices_inst_weaken [in MetaRocq.Erasure.ErasureFunction]
on_minductive_wf_params_weaken [in MetaRocq.Erasure.ErasureFunction]
on_udecl_on_udecl_prop [in MetaRocq.PCUIC.PCUICWeakeningEnv]
on_universes_true [in MetaRocq.SafeChecker.PCUICEqualityDec]
on_one_decl_test_decl [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_test_impl [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_mapi_context [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_map [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_map_na [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_impl [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_free_vars_ctx_onctx_k [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
on_free_vars_ind_predicate_context [in MetaRocq.SafeChecker.PCUICSafeRetyping]
on_free_vars_decl_lift_impl [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
on_free_vars_decl_lift [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
on_free_vars_decl_eq [in MetaRocq.PCUIC.PCUICContextConversion]
on_free_vars_any_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
on_free_vars_ctx_fix_context_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
on_ctx_free_vars_fix_context_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
on_free_vars_ctx_inst_case_context_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
on_ctx_free_vars_inst_case_context_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
on_free_vars_ctx_closed_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
on_global_decls_prefix [in MetaRocq.Erasure.ErasureFunctionProperties]
on_global_env_ind [in MetaRocq.Erasure.ErasureFunctionProperties]
on_free_vars_projs [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_mon [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_to_extended_list_k [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_case_predicate_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_expand_lets_k [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_subst_k [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ind_params [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_cstr_branch_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ind_predicate_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_k_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_decl_trans_on_free_vars_decl [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_constructor_closed_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_udecl_prop_poly_bounded [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_projections_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_inst_pars_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_inst [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_inst_wf_args [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_subst [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_wf_args [in MetaRocq.PCUIC.PCUICInductiveInversion]
on_free_vars_ctx_inst_case_context_xpred0 [in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_ctx_snoc_def_inv [in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_ctx_snoc_ass_inv [in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_subst [in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_shiftnP_S [in MetaRocq.PCUIC.PCUICConversion]
on_fvs_letin [in MetaRocq.PCUIC.PCUICConversion]
on_fvs_lambda [in MetaRocq.PCUIC.PCUICConversion]
on_fvs_prod [in MetaRocq.PCUIC.PCUICConversion]
on_minductive_wf_params [in MetaRocq.PCUIC.PCUICArities]
on_free_vars_ctx_All_fold_over [in MetaRocq.PCUIC.PCUICAlpha]
on_SomeP [in MetaRocq.Utils.MROption]
on_ctx_free_vars_cons [in MetaRocq.PCUIC.PCUICContextReduction]
on_inst_case_context [in MetaRocq.PCUIC.PCUICContextReduction]
on_snd_eq_id_spec [in MetaRocq.Common.BasicAst]
on_udecl_poly_bounded [in MetaRocq.SafeChecker.PCUICSafeChecker]
on_contexts_subst_ctx [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_firstn_skipn [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_pred1_ctx [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_rename_context [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_fold_context_k [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_context_k [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_refl [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_mapi_inv [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_mapi [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app_inv_left [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_app [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app_inv [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app_ex [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app' [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_impl_ind [in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_impl [in MetaRocq.PCUIC.PCUICParallelReduction]
on_projections_decl [in MetaRocq.PCUIC.PCUICInductives]
on_inductive_sort_inst [in MetaRocq.PCUIC.PCUICInductives]
on_inductive_sort [in MetaRocq.PCUIC.PCUICInductives]
on_inductive_inst [in MetaRocq.PCUIC.PCUICInductives]
on_minductive_wf_params_indices_inst [in MetaRocq.PCUIC.PCUICInductives]
on_minductive_wf_params_indices [in MetaRocq.PCUIC.PCUICInductives]
on_udecl_mono [in MetaRocq.SafeChecker.PCUICWfEnv]
on_ctx_free_vars_xpredT_skipn [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
on_ctx_free_vars_xpredT_snoc [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
on_free_vars_subst_consn [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
on_snd_eq_spec [in MetaRocq.Utils.MRProd]
on_snd_on_snd [in MetaRocq.Utils.MRProd]
on_global_inductive_wf_bodies [in MetaRocq.Template.TypingWf]
on_inductive_wf_params [in MetaRocq.Template.TypingWf]
on_global_inductive_wf_params [in MetaRocq.Template.TypingWf]
on_global_decls_extends_not_fresh [in MetaRocq.Template.TypingWf]
on_global_env_impl [in MetaRocq.Template.TypingWf]
on_global_decl_impl [in MetaRocq.Template.TypingWf]
on_free_vars_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICClassification]
on_universes_subst [in MetaRocq.PCUIC.PCUICWfUniverses]
on_universes_lift [in MetaRocq.PCUIC.PCUICWfUniverses]
on_ctx_free_vars_xpredT [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_prod_inv [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_prod [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_ctx_free_vars_app [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_inst_case_context_nil [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_rename_S [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_all_subst [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_def [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_ass [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_fix_context_weak [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_fix_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_inst_case_context_weak [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_inst_case_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snocS [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc_def [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc_ass [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_app [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_closedP_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_closedP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_any_xpredT [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_All_fold [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context_xpredT [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_smash [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_lift_context0 [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_lift_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context0 [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_vdef [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_vass [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_inst_case_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_fix_context [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_extend [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_xpredT [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_tip [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_concat [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_unfold_cofix [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_cofix_subst [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_unfold_fix [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_fix_subst [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_to_extended_list [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_map2_cstr_args [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_map [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms_inds [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_expand_lets_k [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_extended_subst [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_implP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_all_term [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_mkProd_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_all_term [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_mkApps [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift0_above [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift0 [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst1 [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst_gen [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ext [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_global_decl_wf [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
on_global_env_impl [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
on_snd_eq_id_spec [in MetaRocq.Erasure.ELiftSubst]
on_declared_projection [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_constructor [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_inductive [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_minductive [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_constant [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
optimize_correct [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
optimize_extends_env [in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded_decl_fix [in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded_fix [in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded_decl [in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded [in MetaRocq.Erasure.EReorderCstrs]
optimize_correct [in MetaRocq.Erasure.EReorderCstrs]
optimize_cunfold_cofix [in MetaRocq.Erasure.EReorderCstrs]
optimize_cunfold_fix [in MetaRocq.Erasure.EReorderCstrs]
optimize_cofix_subst [in MetaRocq.Erasure.EReorderCstrs]
optimize_fix_subst [in MetaRocq.Erasure.EReorderCstrs]
optimize_iota_red [in MetaRocq.Erasure.EReorderCstrs]
optimize_substl [in MetaRocq.Erasure.EReorderCstrs]
optimize_csubst [in MetaRocq.Erasure.EReorderCstrs]
optimize_mkApps [in MetaRocq.Erasure.EReorderCstrs]
optimize_env_wf [in MetaRocq.Erasure.EInlineProjections]
optimize_env_expanded [in MetaRocq.Erasure.EInlineProjections]
optimize_env_eq [in MetaRocq.Erasure.EInlineProjections]
optimize_extends_env [in MetaRocq.Erasure.EInlineProjections]
optimize_wellformed [in MetaRocq.Erasure.EInlineProjections]
optimize_wellformed_irrel [in MetaRocq.Erasure.EInlineProjections]
optimize_wellformed_term [in MetaRocq.Erasure.EInlineProjections]
optimize_expanded_decl_irrel [in MetaRocq.Erasure.EInlineProjections]
optimize_expanded_decl [in MetaRocq.Erasure.EInlineProjections]
optimize_expanded_irrel [in MetaRocq.Erasure.EInlineProjections]
optimize_expanded [in MetaRocq.Erasure.EInlineProjections]
optimize_correct [in MetaRocq.Erasure.EInlineProjections]
optimize_cunfold_cofix [in MetaRocq.Erasure.EInlineProjections]
optimize_cunfold_fix [in MetaRocq.Erasure.EInlineProjections]
optimize_cofix_subst [in MetaRocq.Erasure.EInlineProjections]
optimize_fix_subst [in MetaRocq.Erasure.EInlineProjections]
optimize_iota_red [in MetaRocq.Erasure.EInlineProjections]
optimize_substl [in MetaRocq.Erasure.EInlineProjections]
optimize_csubst [in MetaRocq.Erasure.EInlineProjections]
optimize_mkApps [in MetaRocq.Erasure.EInlineProjections]
option_extends_spec [in MetaRocq.Utils.MROption]
option_extendsT [in MetaRocq.Utils.MROption]
option_map_Some [in MetaRocq.Utils.MROption]
option_map_id [in MetaRocq.Utils.MROption]
option_map_ext [in MetaRocq.Utils.MROption]
option_map_two [in MetaRocq.Utils.MROption]
option_default_ext [in MetaRocq.Utils.MROption]
option_map_decl_type_map_decl [in MetaRocq.Common.BasicAst]
option_map_decl_body_map_decl [in MetaRocq.Common.BasicAst]
orPL [in MetaRocq.Utils.MRPred]
orPL [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
orPR [in MetaRocq.Utils.MRPred]
orPR [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
OT_byte.lt_not_eq [in MetaRocq.Utils.bytestring]
OT_byte.lt_trans [in MetaRocq.Utils.bytestring]
OT_byte.eq_trans [in MetaRocq.Utils.bytestring]
OT_byte.eq_sym [in MetaRocq.Utils.bytestring]
OT_byte.eq_refl [in MetaRocq.Utils.bytestring]
| 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) |