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