| 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) |
A (lemma)
abstract_eq_wf [in MetaRocq.Erasure.Typed.Erasure]abstract_env_lookup_correct' [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_level_mem_correct' [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_sortb_correct [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_universeb_correct [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_check_constraints_correct [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_sort_correct [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_universe_correct [in MetaRocq.SafeChecker.PCUICWfEnv]
acc_dlexprod_gen [in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_no_loop [in MetaRocq.Erasure.ErasureFunction]
Acc_fun [in MetaRocq.PCUIC.PCUICSafeLemmata]
acc_dlexmod [in MetaRocq.PCUIC.utils.PCUICUtils]
acc_dlexprod [in MetaRocq.PCUIC.utils.PCUICUtils]
Acc_cored_cored' [in MetaRocq.PCUIC.PCUICSN]
Acc_impl [in MetaRocq.PCUIC.PCUICSN]
Acc_no_loop [in MetaRocq.SafeChecker.PCUICWfReduction]
acyclic_no_loop_add_uctx [in MetaRocq.Common.uGraph]
addnP_strengthen_lift [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
addnP_shiftnP_k [in MetaRocq.PCUIC.PCUICSubstitution]
addnP_closedP [in MetaRocq.PCUIC.PCUICContextReduction]
addnP_xpredT [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
addnP_shiftnP_comm [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_orP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_shiftnP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_add [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP0 [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
add_suffix_cons [in MetaRocq.Erasure.ErasureFunctionProperties]
add_multiple_app [in MetaRocq.Erasure.EWcbvEvalNamed]
add_uctx_make_graph2 [in MetaRocq.Common.uGraph]
add_gc_of_constraint_spec [in MetaRocq.Common.uGraph]
add_uctx_subgraph [in MetaRocq.Common.uGraph]
add_uctx_make_graph [in MetaRocq.Common.uGraph]
add_level_edges_add_cstrs_comm [in MetaRocq.Common.uGraph]
add_level_edges_union [in MetaRocq.Common.uGraph]
add_cstrs_union [in MetaRocq.Common.uGraph]
add_level_edges_spec [in MetaRocq.Common.uGraph]
add_cstrs_spec [in MetaRocq.Common.uGraph]
allbiP [in MetaRocq.Utils.All_Forall]
Alli_impl_le [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
Alli_map_option_out_mapi_Some_spec' [in MetaRocq.PCUIC.PCUICSubstitution]
alli_fold_context_k [in MetaRocq.PCUIC.Syntax.PCUICClosed]
alli_subst_instance [in MetaRocq.PCUIC.PCUICFirstorder]
Alli_helper [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
Alli_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
Alli_nth_hyp [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
Alli_nth_hyp_ind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
alli_fold_context_k_prop [in MetaRocq.Common.BasicAst]
Alli_rev_All_fold [in MetaRocq.Utils.All_Forall]
Alli_All_fold [in MetaRocq.Utils.All_Forall]
Alli_map_option_out_mapi_Some_spec [in MetaRocq.Utils.All_Forall]
Alli_map_id [in MetaRocq.Utils.All_Forall]
Alli_mapi_id [in MetaRocq.Utils.All_Forall]
Alli_mapi_spec [in MetaRocq.Utils.All_Forall]
Alli_All_mix [in MetaRocq.Utils.All_Forall]
Alli_shiftn_inv [in MetaRocq.Utils.All_Forall]
Alli_shiftn [in MetaRocq.Utils.All_Forall]
Alli_rev_nth_error [in MetaRocq.Utils.All_Forall]
Alli_app_inv [in MetaRocq.Utils.All_Forall]
Alli_rev_inv [in MetaRocq.Utils.All_Forall]
Alli_rev [in MetaRocq.Utils.All_Forall]
Alli_refl [in MetaRocq.Utils.All_Forall]
Alli_shift [in MetaRocq.Utils.All_Forall]
Alli_mapi [in MetaRocq.Utils.All_Forall]
Alli_nth_error [in MetaRocq.Utils.All_Forall]
Alli_app [in MetaRocq.Utils.All_Forall]
Alli_All [in MetaRocq.Utils.All_Forall]
Alli_mix [in MetaRocq.Utils.All_Forall]
Alli_impl [in MetaRocq.Utils.All_Forall]
Alli_impl_Alli [in MetaRocq.Utils.All_Forall]
alli_mapi [in MetaRocq.Utils.All_Forall]
alli_map [in MetaRocq.Utils.All_Forall]
alli_shift [in MetaRocq.Utils.All_Forall]
alli_app [in MetaRocq.Utils.All_Forall]
alli_shiftn [in MetaRocq.Utils.All_Forall]
alli_Alli [in MetaRocq.Utils.All_Forall]
alli_impl [in MetaRocq.Utils.All_Forall]
alli_ext [in MetaRocq.Utils.All_Forall]
Alli_id [in MetaRocq.Template.TypingWf]
Alli_map [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Alli_All_mix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Alli_map [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Alli_map_option_out_mapi_Some_spec [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
allowed_eliminations_config_impl [in MetaRocq.Common.Universes]
allowed_eliminations_subset_impl [in MetaRocq.Common.Universes]
All_local_env_Pclosed [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
All_mapi_spec [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
All_mfix_wf [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
All_local_env_inst [in MetaRocq.PCUIC.PCUICSubstitution]
All_local_env_subst [in MetaRocq.PCUIC.PCUICSubstitution]
All_local_assum_subst [in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_app [in MetaRocq.PCUIC.PCUICElimination]
all_rels_subst_lift [in MetaRocq.PCUIC.PCUICSpine]
all_rels_subst [in MetaRocq.PCUIC.PCUICSpine]
all_rels_lift [in MetaRocq.PCUIC.PCUICSpine]
all_rels_length [in MetaRocq.PCUIC.PCUICSpine]
All_map_size [in MetaRocq.PCUIC.PCUICTyping]
All_All2_diag [in MetaRocq.SafeChecker.PCUICEqualityDec]
All_All2_telescopei [in MetaRocq.PCUIC.PCUICConfluence]
All_All2_telescopei_gen [in MetaRocq.PCUIC.PCUICConfluence]
All_fold_fold_context_k_defs [in MetaRocq.Template.EtaExpand]
all_closed [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All_local_env_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_over_All [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_closed_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_map_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_local_env_app_l [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
All_decls_alpha_pb_map [in MetaRocq.PCUIC.PCUICConversion]
All_decls_alpha_pb_impl [in MetaRocq.PCUIC.PCUICConversion]
All_fold_nth_error [in MetaRocq.PCUIC.PCUICEtaExpand]
All_fold_map_context [in MetaRocq.PCUIC.PCUICEtaExpand]
All_decls_alpha_pb_ws_decl [in MetaRocq.PCUIC.PCUICAlpha]
All_eval_etaexp [in MetaRocq.Erasure.EEtaExpandedFix]
all_isEtaExp_closedn [in MetaRocq.Erasure.EEtaExpandedFix]
All_reorder_list [in MetaRocq.Erasure.EReorderCstrs]
All_depth [in MetaRocq.PCUIC.Syntax.PCUICDepth]
All_All2_fold_swap [in MetaRocq.Utils.All_Forall]
All_All2_fold_swap_sum [in MetaRocq.Utils.All_Forall]
All_All2_swap [in MetaRocq.Utils.All_Forall]
All_All2_swap_sum [in MetaRocq.Utils.All_Forall]
All_eta3 [in MetaRocq.Utils.All_Forall]
All_Alli_swap_iff [in MetaRocq.Utils.All_Forall]
All_map_All [in MetaRocq.Utils.All_Forall]
All_remove_last [in MetaRocq.Utils.All_Forall]
All_fold_All2_fold [in MetaRocq.Utils.All_Forall]
All_fold_All2_fold_impl [in MetaRocq.Utils.All_Forall]
All_fold_prod [in MetaRocq.Utils.All_Forall]
All_fold_Alli_rev [in MetaRocq.Utils.All_Forall]
All_fold_app [in MetaRocq.Utils.All_Forall]
All_fold_impl [in MetaRocq.Utils.All_Forall]
All_fold_app_inv [in MetaRocq.Utils.All_Forall]
All_fold_tip [in MetaRocq.Utils.All_Forall]
All_forall [in MetaRocq.Utils.All_Forall]
All_In [in MetaRocq.Utils.All_Forall]
All_All2_refl [in MetaRocq.Utils.All_Forall]
All_sq [in MetaRocq.Utils.All_Forall]
All_prod [in MetaRocq.Utils.All_Forall]
All_pair [in MetaRocq.Utils.All_Forall]
All_prod_inv [in MetaRocq.Utils.All_Forall]
All_forallb_eq_forallb [in MetaRocq.Utils.All_Forall]
All_forallb_forallb_spec [in MetaRocq.Utils.All_Forall]
All_forallb_map_spec [in MetaRocq.Utils.All_Forall]
All_All2_All2_mix [in MetaRocq.Utils.All_Forall]
All_All2 [in MetaRocq.Utils.All_Forall]
All_repeat [in MetaRocq.Utils.All_Forall]
All_All_All2 [in MetaRocq.Utils.All_Forall]
All_All2_flex [in MetaRocq.Utils.All_Forall]
All_Alli [in MetaRocq.Utils.All_Forall]
All_mapi [in MetaRocq.Utils.All_Forall]
All_forallb' [in MetaRocq.Utils.All_Forall]
All_map_id' [in MetaRocq.Utils.All_Forall]
All_safe_nth [in MetaRocq.Utils.All_Forall]
All_map_id [in MetaRocq.Utils.All_Forall]
All_map_eq [in MetaRocq.Utils.All_Forall]
All_reflect_reflect_All2 [in MetaRocq.Utils.All_Forall]
All_nth_error [in MetaRocq.Utils.All_Forall]
All_map_inv [in MetaRocq.Utils.All_Forall]
All_map [in MetaRocq.Utils.All_Forall]
All_impl [in MetaRocq.Utils.All_Forall]
All_impl_All [in MetaRocq.Utils.All_Forall]
All_rev_inv [in MetaRocq.Utils.All_Forall]
All_rev [in MetaRocq.Utils.All_Forall]
All_rev_map [in MetaRocq.Utils.All_Forall]
All_refl [in MetaRocq.Utils.All_Forall]
All_mix [in MetaRocq.Utils.All_Forall]
All_tip [in MetaRocq.Utils.All_Forall]
All_True [in MetaRocq.Utils.All_Forall]
All_app_inv [in MetaRocq.Utils.All_Forall]
All_app [in MetaRocq.Utils.All_Forall]
All_skipn [in MetaRocq.Utils.All_Forall]
All_firstn [in MetaRocq.Utils.All_Forall]
All_forallb [in MetaRocq.Utils.All_Forall]
All_Forall [in MetaRocq.Utils.All_Forall]
All_decls_on_free_vars_map_impl [in MetaRocq.PCUIC.PCUICParallelReduction]
All_fold_fold_context_k [in MetaRocq.PCUIC.PCUICParallelReduction]
All_decls_on_free_vars_impl [in MetaRocq.PCUIC.PCUICParallelReduction]
All_decls_map [in MetaRocq.PCUIC.PCUICParallelReduction]
All_or_disj [in MetaRocq.PCUIC.PCUICProgress]
all_rels_smash [in MetaRocq.PCUIC.PCUICInductives]
All_decls_map_right [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_decls_on_free_vars_map_impl_inv [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_rho [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_gen_rho [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_IH' [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_IH [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_local_env_wf_decls [in MetaRocq.Template.TypingWf]
All_Alli [in MetaRocq.Template.TypingWf]
All_mapi [in MetaRocq.Template.TypingWf]
All_local_env_wf_decl_inv [in MetaRocq.Template.TypingWf]
All_local_env_wf_decl [in MetaRocq.Template.TypingWf]
All_local_env_over_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
All_masked [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
All_over_All [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All_fold_on_free_vars_ctx [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
All_All2_refl [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All_map_option_out_map_Some_spec [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All_map2 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All_fold_All_mix_left [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
All_fold_map [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
All1i_Alli_mix_left [in MetaRocq.Utils.All_Forall]
All1i_map2_right [in MetaRocq.Utils.All_Forall]
All1_map2_right [in MetaRocq.Utils.All_Forall]
All1_map2_right_inv [in MetaRocq.Utils.All_Forall]
All2i_map [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
All2i_All2 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_sym [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_All2_mapi [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map_left_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map_right_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_prod [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
All2i_Alli_mix_left [in MetaRocq.Utils.All_Forall]
All2i_map2_right [in MetaRocq.Utils.All_Forall]
All2i_All2_All2 [in MetaRocq.Utils.All_Forall]
All2i_All2_All2i_All2i [in MetaRocq.Utils.All_Forall]
All2i_All2 [in MetaRocq.Utils.All_Forall]
All2i_app_inv [in MetaRocq.Utils.All_Forall]
All2i_length [in MetaRocq.Utils.All_Forall]
All2i_app_inv_r [in MetaRocq.Utils.All_Forall]
All2i_app_inv_l [in MetaRocq.Utils.All_Forall]
All2i_nth_error_r [in MetaRocq.Utils.All_Forall]
All2i_nth_error_l [in MetaRocq.Utils.All_Forall]
All2i_nth_hyp [in MetaRocq.Utils.All_Forall]
All2i_nth_impl_gen [in MetaRocq.Utils.All_Forall]
All2i_map_right [in MetaRocq.Utils.All_Forall]
All2i_map [in MetaRocq.Utils.All_Forall]
All2i_rev_ctx_inv [in MetaRocq.Utils.All_Forall]
All2i_rev_ctx_gen [in MetaRocq.Utils.All_Forall]
All2i_rev_ctx [in MetaRocq.Utils.All_Forall]
All2i_len_rev [in MetaRocq.Utils.All_Forall]
All2i_len_impl [in MetaRocq.Utils.All_Forall]
All2i_len_length [in MetaRocq.Utils.All_Forall]
All2i_len_app [in MetaRocq.Utils.All_Forall]
All2i_rev [in MetaRocq.Utils.All_Forall]
All2i_trivial [in MetaRocq.Utils.All_Forall]
All2i_mapi_rec [in MetaRocq.Utils.All_Forall]
All2i_app [in MetaRocq.Utils.All_Forall]
All2i_mapi [in MetaRocq.Utils.All_Forall]
All2i_impl [in MetaRocq.Utils.All_Forall]
All2i_All_right [in MetaRocq.Utils.All_Forall]
All2i_All_left [in MetaRocq.Utils.All_Forall]
All2i_All2_mix_left [in MetaRocq.Utils.All_Forall]
All2i_All_mix_right [in MetaRocq.Utils.All_Forall]
All2i_All_mix_left [in MetaRocq.Utils.All_Forall]
All2i_nth_error [in MetaRocq.Utils.All_Forall]
All2i_All2i_mix [in MetaRocq.Utils.All_Forall]
All2i_All2 [in MetaRocq.Template.TypingWf]
All2i_sym [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2i_All2_mapi [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2P [in MetaRocq.Utils.All_Forall]
All2_fold_nth_ass [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
All2_eq_context_upto [in MetaRocq.PCUIC.PCUICEquality]
All2_ctx_inst [in MetaRocq.PCUIC.PCUICSpine]
All2_fold_mapi_right [in MetaRocq.PCUIC.PCUICSpine]
All2_many_OnOne2 [in MetaRocq.PCUIC.utils.PCUICOnOne]
All2_nil_rev [in MetaRocq.Template.WcbvEval]
All2_nil [in MetaRocq.Template.WcbvEval]
All2_cumul_over_refl [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
All2_conv_over_refl [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
All2_eq_binder_subst_context_inst [in MetaRocq.PCUIC.PCUICValidity]
All2_fold_red_refl [in MetaRocq.PCUIC.PCUICContextConversion]
All2_fold_over_red_refl [in MetaRocq.PCUIC.PCUICContextConversion]
All2_All2_fold_fix_context [in MetaRocq.PCUIC.PCUICConfluence]
All2_fold_refl [in MetaRocq.PCUIC.PCUICConfluence]
All2_eval_snoc_elim [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_rev_rect [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_split_eq [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_map_option_out_mapi_Some_spec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2_eq_binder_expand_lets_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2_eq_binder_lift_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2_sym [in MetaRocq.PCUIC.PCUICInductiveInversion]
All2_fold_context_k [in MetaRocq.PCUIC.PCUICInductiveInversion]
All2_fold_inst [in MetaRocq.PCUIC.PCUICInductiveInversion]
All2_fold_over_same_app [in MetaRocq.PCUIC.PCUICConversion]
All2_fold_over_same [in MetaRocq.PCUIC.PCUICConversion]
All2_fold_fold_context_k [in MetaRocq.PCUIC.PCUICConversion]
All2_many_OnOne2_pres [in MetaRocq.PCUIC.PCUICConversion]
All2_fold_All_right [in MetaRocq.PCUIC.PCUICAlpha]
All2_fold_All_fold_mix_right [in MetaRocq.PCUIC.PCUICAlpha]
All2_fold_cst_map [in MetaRocq.Common.BasicAst]
All2_fold_map [in MetaRocq.Common.BasicAst]
All2_fold_mapi [in MetaRocq.Common.BasicAst]
All2_fold_impl_onctx [in MetaRocq.Common.BasicAst]
All2_eq_binder_subst_instance [in MetaRocq.PCUIC.PCUICCasesContexts]
All2_eq_binder_subst_context [in MetaRocq.PCUIC.PCUICCasesContexts]
All2_map2_right_inv [in MetaRocq.Utils.All_Forall]
All2_map2_right [in MetaRocq.Utils.All_Forall]
All2_fold_All_swap [in MetaRocq.Utils.All_Forall]
All2_All_swap [in MetaRocq.Utils.All_Forall]
All2_map2_left_All3 [in MetaRocq.Utils.All_Forall]
All2_map2_left [in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_inv [in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix [in MetaRocq.Utils.All_Forall]
All2_fold_prod_inv [in MetaRocq.Utils.All_Forall]
All2_fold_prod [in MetaRocq.Utils.All_Forall]
All2_fold_nth_r [in MetaRocq.Utils.All_Forall]
All2_fold_nth [in MetaRocq.Utils.All_Forall]
All2_fold_forallb2 [in MetaRocq.Utils.All_Forall]
All2_fold_impl_len [in MetaRocq.Utils.All_Forall]
All2_fold_impl_ind [in MetaRocq.Utils.All_Forall]
All2_fold_app_inv_l [in MetaRocq.Utils.All_Forall]
All2_fold_app_inv [in MetaRocq.Utils.All_Forall]
All2_fold_flip [in MetaRocq.Utils.All_Forall]
All2_fold_sym [in MetaRocq.Utils.All_Forall]
All2_fold_trans [in MetaRocq.Utils.All_Forall]
All2_fold_refl [in MetaRocq.Utils.All_Forall]
All2_fold_All2 [in MetaRocq.Utils.All_Forall]
All2_fold_All_left [in MetaRocq.Utils.All_Forall]
All2_fold_All_right [in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_left_inv [in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_right [in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_left [in MetaRocq.Utils.All_Forall]
All2_fold_impl [in MetaRocq.Utils.All_Forall]
All2_fold_length [in MetaRocq.Utils.All_Forall]
All2_fold_app [in MetaRocq.Utils.All_Forall]
All2_fold_from_nth_error [in MetaRocq.Utils.All_Forall]
All2_In_right [in MetaRocq.Utils.All_Forall]
All2_In [in MetaRocq.Utils.All_Forall]
All2_app_r [in MetaRocq.Utils.All_Forall]
All2_sq [in MetaRocq.Utils.All_Forall]
All2_eq [in MetaRocq.Utils.All_Forall]
All2_nth_error_Some_right [in MetaRocq.Utils.All_Forall]
All2_symP [in MetaRocq.Utils.All_Forall]
All2_sym [in MetaRocq.Utils.All_Forall]
All2_prod_inv [in MetaRocq.Utils.All_Forall]
All2_prod [in MetaRocq.Utils.All_Forall]
All2_same [in MetaRocq.Utils.All_Forall]
All2_nth_error_Some_r [in MetaRocq.Utils.All_Forall]
All2_nth_error_Some [in MetaRocq.Utils.All_Forall]
All2_impl' [in MetaRocq.Utils.All_Forall]
All2_firstn [in MetaRocq.Utils.All_Forall]
All2_swap [in MetaRocq.Utils.All_Forall]
All2_dep_nth_error [in MetaRocq.Utils.All_Forall]
All2_dep_from_nth_error [in MetaRocq.Utils.All_Forall]
All2_nth_error [in MetaRocq.Utils.All_Forall]
All2_from_nth_error [in MetaRocq.Utils.All_Forall]
All2_right_triv [in MetaRocq.Utils.All_Forall]
All2_skipn [in MetaRocq.Utils.All_Forall]
All2_mapi [in MetaRocq.Utils.All_Forall]
All2_nth [in MetaRocq.Utils.All_Forall]
All2_trans' [in MetaRocq.Utils.All_Forall]
All2_trans [in MetaRocq.Utils.All_Forall]
All2_All [in MetaRocq.Utils.All_Forall]
All2_impl_In [in MetaRocq.Utils.All_Forall]
All2_rev [in MetaRocq.Utils.All_Forall]
All2_app [in MetaRocq.Utils.All_Forall]
All2_ind_rev [in MetaRocq.Utils.All_Forall]
All2_rect_rev [in MetaRocq.Utils.All_Forall]
All2_app_inv [in MetaRocq.Utils.All_Forall]
All2_app_inv_r [in MetaRocq.Utils.All_Forall]
All2_app_inv_l [in MetaRocq.Utils.All_Forall]
All2_nth_error_None [in MetaRocq.Utils.All_Forall]
All2_length [in MetaRocq.Utils.All_Forall]
All2_All_left_pack [in MetaRocq.Utils.All_Forall]
All2_non_nil [in MetaRocq.Utils.All_Forall]
All2_reflect_reflect_All2 [in MetaRocq.Utils.All_Forall]
All2_mix_inv [in MetaRocq.Utils.All_Forall]
All2_mix [in MetaRocq.Utils.All_Forall]
All2_All2_mix [in MetaRocq.Utils.All_Forall]
All2_undep [in MetaRocq.Utils.All_Forall]
All2_map_right [in MetaRocq.Utils.All_Forall]
All2_map_left' [in MetaRocq.Utils.All_Forall]
All2_map_left [in MetaRocq.Utils.All_Forall]
All2_map_right_equiv [in MetaRocq.Utils.All_Forall]
All2_map_left_equiv [in MetaRocq.Utils.All_Forall]
All2_Forall2 [in MetaRocq.Utils.All_Forall]
All2_dep_impl [in MetaRocq.Utils.All_Forall]
All2_apply_dep_All [in MetaRocq.Utils.All_Forall]
All2_apply_dep_arrow [in MetaRocq.Utils.All_Forall]
All2_apply_arrow [in MetaRocq.Utils.All_Forall]
All2_apply [in MetaRocq.Utils.All_Forall]
All2_transitivity [in MetaRocq.Utils.All_Forall]
All2_symmetry [in MetaRocq.Utils.All_Forall]
All2_reflexivity [in MetaRocq.Utils.All_Forall]
All2_eq_eq [in MetaRocq.Utils.All_Forall]
All2_impl [in MetaRocq.Utils.All_Forall]
All2_impl_All2 [in MetaRocq.Utils.All_Forall]
All2_right [in MetaRocq.Utils.All_Forall]
All2_All_right [in MetaRocq.Utils.All_Forall]
All2_All_left [in MetaRocq.Utils.All_Forall]
All2_All2_All2 [in MetaRocq.Utils.All_Forall]
All2_All_mix_right [in MetaRocq.Utils.All_Forall]
All2_All_mix_left [in MetaRocq.Utils.All_Forall]
All2_tip_l [in MetaRocq.Utils.All_Forall]
All2_map_inv [in MetaRocq.Utils.All_Forall]
All2_map [in MetaRocq.Utils.All_Forall]
All2_map_equiv [in MetaRocq.Utils.All_Forall]
All2_refl [in MetaRocq.Utils.All_Forall]
All2_forallb2 [in MetaRocq.Utils.All_Forall]
All2_tip [in MetaRocq.Utils.All_Forall]
All2_All2_prop2_eq [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_All2_prop_eq [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_branch_prop [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_All2_prop [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_over_impl [in MetaRocq.Erasure.EWcbvEval]
All2_ind_OnOne2 [in MetaRocq.PCUIC.PCUICReduction]
All2_eq [in MetaRocq.PCUIC.PCUICReduction]
All2_fold_fold_context_right [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_fold_context_assumptions [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_mapi [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_prop2_eq_split [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_masked [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
All2_map_option_out_mapi_Some_spec [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_eq_binder_expand_lets_ctx [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_eq_binder_lift_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_refl_inv [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_All_map2 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_nth_hyp [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_All2_All2_All3 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_map2 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_map_option_out_mapi_Some_spec [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_over_undep [in MetaRocq.Erasure.EPrimitive]
All2_All2_Set [in MetaRocq.Erasure.EPrimitive]
All2_Set_All2 [in MetaRocq.Erasure.EPrimitive]
All3P [in MetaRocq.Utils.All_Forall]
All3_impl [in MetaRocq.PCUIC.PCUICNormal]
All3_impl [in MetaRocq.Utils.All_Forall]
All3_map_all [in MetaRocq.Utils.All_Forall]
All3_Forall3 [in MetaRocq.Utils.All_Forall]
All3_forallb3 [in MetaRocq.Utils.All_Forall]
All3_many_OnOne2All [in MetaRocq.PCUIC.PCUICReduction]
All3_length [in MetaRocq.PCUIC.PCUICReduction]
alpha_eq_subst_context [in MetaRocq.Template.TermEquality]
alpha_eq_extended_subst [in MetaRocq.Template.TermEquality]
alpha_eq_context_assumptions [in MetaRocq.Template.TermEquality]
alpha_eq_context_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICSafeLemmata]
alpha_eq_context_closed [in MetaRocq.PCUIC.PCUICSafeLemmata]
alpha_eq_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
alpha_eq_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
alpha_eq_subst_context [in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_lift_context [in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_smash_context [in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_extended_subst [in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_context_assumptions [in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_subst_instance [in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_trans [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
alpha_eq_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
alt_into_ws_cumul_pb_terms [in MetaRocq.PCUIC.PCUICConvCumInversion]
andb_andI [in MetaRocq.Utils.MRProd]
andb_and [in MetaRocq.Utils.MRProd]
andb_is_true [in MetaRocq.Common.uGraph]
anonymize_two [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
append_Empty_r [in MetaRocq.Erasure.EWcbvEvalNamed]
append_inv [in MetaRocq.Erasure.EWcbvEvalNamed]
application_atom_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
apply_expanded [in MetaRocq.Erasure.ErasureFunctionProperties]
apply_expanded [in MetaRocq.Template.EtaExpand]
app_tip_nil [in MetaRocq.Utils.MRList]
app_inj_length_l [in MetaRocq.Utils.MRList]
app_inj_length_r [in MetaRocq.Utils.MRList]
app_tip_assoc [in MetaRocq.Utils.MRList]
app_cored_r [in MetaRocq.PCUIC.PCUICSafeLemmata]
app_mkApps [in MetaRocq.PCUIC.PCUICConversion]
app_context_length [in MetaRocq.Common.BasicAst]
app_context_push [in MetaRocq.Common.BasicAst]
app_context_cons [in MetaRocq.Common.BasicAst]
app_context_assoc [in MetaRocq.Common.BasicAst]
app_context_nil_l [in MetaRocq.Common.BasicAst]
app_Forall [in MetaRocq.Utils.All_Forall]
app_inj [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
arguments_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
arguments_mkApps_nApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
AritiesToGeneration_typing_spine [in MetaRocq.PCUIC.PCUICCasesHelper]
arities_contexts_1 [in MetaRocq.Erasure.Typed.Erasure]
arities_contexts_cons_1 [in MetaRocq.Erasure.Typed.Erasure]
arity_spine_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_eq [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_it_mkProd_or_LetIn_Sort [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICSpine]
arity_typing_spine [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_to_extended_list_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
arity_spine_to_extended_list [in MetaRocq.PCUIC.PCUICInductiveInversion]
arity_spine_eq [in MetaRocq.PCUIC.PCUICInductiveInversion]
arity_red_to_prod_or_sort [in MetaRocq.PCUIC.PCUICConversion]
arity_spine_case_predicate [in MetaRocq.PCUIC.PCUICInductives]
arity_type_inv [in MetaRocq.Erasure.EArities]
assumption_context_compare_decls [in MetaRocq.Erasure.Prelim]
assumption_context_cstr_branch_context [in MetaRocq.Erasure.Prelim]
assumption_context_map2_binders [in MetaRocq.Erasure.Prelim]
assumption_context_arity_ass_context [in MetaRocq.SafeChecker.PCUICSafeReduce]
assumption_context_skipn [in MetaRocq.PCUIC.PCUICSubstitution]
assumption_context_app_inv [in MetaRocq.PCUIC.Syntax.PCUICClosed]
assumption_context_arities_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
assumption_context_assumptions [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
assumption_context_lift_context [in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_subst_context [in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_expand_lets_ctx [in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_subst_instance [in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_map [in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_fold [in MetaRocq.PCUIC.PCUICContexts]
assumption_context_length [in MetaRocq.PCUIC.PCUICContexts]
assumption_context_app [in MetaRocq.PCUIC.PCUICSigmaCalculus]
assumption_context_firstn [in MetaRocq.PCUIC.PCUICClassification]
assumption_context_assumptions [in MetaRocq.PCUIC.PCUICClassification]
assumption_context_rev [in MetaRocq.SafeChecker.PCUICTypeChecker]
assumption_context_subst_telescope [in MetaRocq.SafeChecker.PCUICTypeChecker]
Ast_inst_case_context_assumptions [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Ast_inst_case_context_length [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Ast_cstr_branch_context_assumptions [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
atom_decompose_app [in MetaRocq.Template.AstUtils]
atom_nApp [in MetaRocq.Template.WcbvEval]
atom_mkApps [in MetaRocq.Template.WcbvEval]
atom_decompose_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
atom_nApp [in MetaRocq.Erasure.EWcbvEval]
atom_mkApps [in MetaRocq.Erasure.EWcbvEval]
atom_mkApps [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
atom_nApp [in MetaRocq.PCUIC.PCUICWcbvEval]
atom_mkApps [in MetaRocq.PCUIC.PCUICWcbvEval]
atpos_assoc [in MetaRocq.PCUIC.Syntax.PCUICPosition]
axiom_free_value_mkApps [in MetaRocq.PCUIC.PCUICClassification]
axiom_free_axiom_free_value [in MetaRocq.PCUIC.PCUICClassification]
| 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) |