| 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) |
M (lemma)
make_context_subst_context_assumptions [in MetaRocq.PCUIC.PCUICContextSubst]make_context_subst_spec_inv [in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_recP [in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_spec [in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_rec_spec [in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_length [in MetaRocq.PCUIC.PCUICSpine]
make_context_subst_tele [in MetaRocq.PCUIC.PCUICSpine]
make_context_subst_skipn [in MetaRocq.PCUIC.PCUICSpine]
make_graph_spec2 [in MetaRocq.Common.uGraph]
make_graph_spec' [in MetaRocq.Common.uGraph]
make_graph_spec [in MetaRocq.Common.uGraph]
make_graph_E [in MetaRocq.Common.uGraph]
make_typing_spine [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
mapi_map2 [in MetaRocq.Utils.MRList]
mapi_unfold [in MetaRocq.Utils.MRList]
mapi_irrel_list [in MetaRocq.Utils.MRList]
mapi_nth [in MetaRocq.Utils.MRList]
mapi_cons [in MetaRocq.Utils.MRList]
mapi_length [in MetaRocq.Utils.MRList]
mapi_rec_length [in MetaRocq.Utils.MRList]
mapi_rev [in MetaRocq.Utils.MRList]
mapi_rec_rev [in MetaRocq.Utils.MRList]
mapi_app [in MetaRocq.Utils.MRList]
mapi_rec_app [in MetaRocq.Utils.MRList]
mapi_rec_add [in MetaRocq.Utils.MRList]
mapi_rec_Sk [in MetaRocq.Utils.MRList]
mapi_ext [in MetaRocq.Utils.MRList]
mapi_rec_ext [in MetaRocq.Utils.MRList]
mapi_cst_map [in MetaRocq.Utils.MRList]
mapi_mapi [in MetaRocq.Utils.MRList]
mapi_map [in MetaRocq.Utils.MRList]
mapi_rec_eqn [in MetaRocq.Utils.MRList]
mapi_compose [in MetaRocq.Utils.MRList]
mapi_rec_compose [in MetaRocq.Utils.MRList]
mapi_ext_size [in MetaRocq.Utils.MRList]
mapi_context_compose [in MetaRocq.PCUIC.PCUICSigmaCalculus]
mapi_context_map_context [in MetaRocq.Common.BasicAst]
mapi_context_map [in MetaRocq.Common.BasicAst]
mapi_context_In_spec [in MetaRocq.Common.BasicAst]
mapi_context_fold [in MetaRocq.Common.BasicAst]
mapi_context_length [in MetaRocq.Common.BasicAst]
mapi_context_eqP_test_id_spec [in MetaRocq.PCUIC.PCUICAst]
mapi_context_eqP_id_spec [in MetaRocq.PCUIC.PCUICAst]
mapi_context_eqP_spec [in MetaRocq.PCUIC.PCUICAst]
mapi_context_subst [in MetaRocq.PCUIC.PCUICParallelReduction]
mapi_context_lift [in MetaRocq.PCUIC.PCUICParallelReduction]
mapi_context_rename [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
mapi_context_fold_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
mapi_context_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
mapi_context_eqP_onctx_k_spec [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
mapOne [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
mapOne [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
mapopt_option_map [in MetaRocq.Erasure.EReorderCstrs]
mapopt_inv_spec [in MetaRocq.Erasure.EReorderCstrs]
mapopt_spec [in MetaRocq.Erasure.EReorderCstrs]
mapu_array_model_proper_cond [in MetaRocq.PCUIC.PCUICAst]
mapu_array_model_proper [in MetaRocq.PCUIC.PCUICAst]
mapu_prim_compose_rew [in MetaRocq.PCUIC.PCUICAst]
mapu_prim_compose [in MetaRocq.PCUIC.PCUICAst]
map_squash [in MetaRocq.Utils.MRSquash]
map_const [in MetaRocq.PCUIC.Syntax.PCUICPosition]
map_subst_lift0_subst [in MetaRocq.PCUIC.PCUICSR]
map_expand_lets_to_extended_list [in MetaRocq.PCUIC.PCUICSR]
map_map2 [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map_anon_fold_context_k [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map_def_sig_nl [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map_subst_instance_to_extended_list_k [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_app_simpl [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_subst_lift_lift [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_ext [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_id_eq [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_id [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_lift_lift [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_vass_map_def [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_lift0 [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_repeat [in MetaRocq.Utils.MRList]
map_InP_spec [in MetaRocq.Utils.MRList]
map_mapIn_eq [in MetaRocq.Utils.MRList]
map_In_ext [in MetaRocq.Utils.MRList]
map_map_In [in MetaRocq.Utils.MRList]
map_In_spec [in MetaRocq.Utils.MRList]
map_inj [in MetaRocq.Utils.MRList]
map_mapi [in MetaRocq.Utils.MRList]
map_nil [in MetaRocq.Utils.MRList]
map_skipn [in MetaRocq.Utils.MRList]
map_ext [in MetaRocq.Utils.MRList]
map_ext_size [in MetaRocq.Utils.MRList]
map_id_f [in MetaRocq.Utils.MRList]
map_cst_repeat [in MetaRocq.Utils.MRList]
map_map_compose [in MetaRocq.Utils.MRList]
map_option_out_impl [in MetaRocq.PCUIC.PCUICSubstitution]
map_vass_map_def_subst [in MetaRocq.PCUIC.PCUICSubstitution]
map_subst_closedn [in MetaRocq.PCUIC.Syntax.PCUICClosed]
map_decl_closed_ext [in MetaRocq.PCUIC.Syntax.PCUICClosed]
map_subst_lift1 [in MetaRocq.PCUIC.PCUICSpine]
map_subst_extended_subst [in MetaRocq.PCUIC.PCUICSpine]
map_subst_extended_subst_lift_to_extended_list_k [in MetaRocq.PCUIC.PCUICSpine]
map_unbox_repeat_box [in MetaRocq.Erasure.EUnboxing]
map_repeat [in MetaRocq.Erasure.EUnboxing]
map_InP_length [in MetaRocq.PCUIC.utils.PCUICAstUtils]
map_InP_spec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
map_erase_length [in MetaRocq.Erasure.ErasureFunctionProperties]
map_erase_irrel [in MetaRocq.Erasure.ErasureFunctionProperties]
map_expand_lets_to_extended_list_k_above [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_expand_lets_lift_cancel [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_option_out_check_one_cofix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_option_out_check_one_fix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_context_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_map2 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_vass_map_def [in MetaRocq.Template.LiftSubst]
map_non_nil [in MetaRocq.Template.LiftSubst]
map_branches_k_map_branches_k [in MetaRocq.Template.LiftSubst]
map_map_subst_expand_lets [in MetaRocq.PCUIC.PCUICInductiveInversion]
map_branches_k_map_branches_k [in MetaRocq.PCUIC.PCUICConversion]
map_subst_instance_to_extended_list_k [in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
map_vass_map_def [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
map_option_out_impl [in MetaRocq.Utils.MROption]
map_option_out_length [in MetaRocq.Utils.MROption]
map_option_out_map_option_map [in MetaRocq.Utils.MROption]
map_reln_ext [in MetaRocq.PCUIC.PCUICContexts]
map_subst_app_decomp [in MetaRocq.PCUIC.PCUICContexts]
map_subst_app_to_extended_list_k [in MetaRocq.PCUIC.PCUICContexts]
map_subst_instance_to_extended_list_k [in MetaRocq.PCUIC.PCUICContexts]
map_subst_expand_lets_k [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_subst_expand_lets [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_expand_lets_subst_comm [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_subst_inst [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_idsn_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_inst_idsn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_map_branch_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_map_predicate_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate_gen [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_id_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_id_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_eq_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_eq_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_bcontext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_bbody [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_puinst [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_pcontext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_preturn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_pparams [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_decl_name_fold_context_k [in MetaRocq.Common.BasicAst]
map_context_id [in MetaRocq.Common.BasicAst]
map_mapi_context [in MetaRocq.Common.BasicAst]
map_map_context [in MetaRocq.Common.BasicAst]
map_context_map [in MetaRocq.Common.BasicAst]
map_context_mapi_context [in MetaRocq.Common.BasicAst]
map_fold_context_k [in MetaRocq.Common.BasicAst]
map_decl_id [in MetaRocq.Common.BasicAst]
map_decl_body [in MetaRocq.Common.BasicAst]
map_decl_type [in MetaRocq.Common.BasicAst]
map_context_length [in MetaRocq.Common.BasicAst]
map_decl_ext [in MetaRocq.Common.BasicAst]
map_def_id_spec [in MetaRocq.Common.BasicAst]
map_def_eq_spec [in MetaRocq.Common.BasicAst]
map_def_spec [in MetaRocq.Common.BasicAst]
map_def_id [in MetaRocq.Common.BasicAst]
map_def_map_def [in MetaRocq.Common.BasicAst]
map_dbody [in MetaRocq.Common.BasicAst]
map_dtype [in MetaRocq.Common.BasicAst]
map_context_eqP_spec [in MetaRocq.PCUIC.PCUICAst]
map_decl_eqP_spec [in MetaRocq.PCUIC.PCUICAst]
map_branches_k_map_branches_k [in MetaRocq.PCUIC.PCUICAst]
map_branches_map_branches [in MetaRocq.PCUIC.PCUICAst]
map_branch_k_id_spec [in MetaRocq.PCUIC.PCUICAst]
map_branch_id_spec [in MetaRocq.PCUIC.PCUICAst]
map_branch_k_eq_spec [in MetaRocq.PCUIC.PCUICAst]
map_branch_eq_spec [in MetaRocq.PCUIC.PCUICAst]
map_context_eq_spec [in MetaRocq.PCUIC.PCUICAst]
map_decl_eq_spec [in MetaRocq.PCUIC.PCUICAst]
map_branch_id [in MetaRocq.PCUIC.PCUICAst]
map_branch_k_map_branch [in MetaRocq.PCUIC.PCUICAst]
map_branch_map_branch_k [in MetaRocq.PCUIC.PCUICAst]
map_branch_k_map_branch_k_id [in MetaRocq.PCUIC.PCUICAst]
map_branch_k_map_branch_k [in MetaRocq.PCUIC.PCUICAst]
map_branch_map_branch [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_map_predicate [in MetaRocq.PCUIC.PCUICAst]
map_predicate_map_predicate_k [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_map_predicate_k [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_id_spec [in MetaRocq.PCUIC.PCUICAst]
map_predicate_id_spec [in MetaRocq.PCUIC.PCUICAst]
map_context_id_spec_cond [in MetaRocq.PCUIC.PCUICAst]
map_context_id_spec [in MetaRocq.PCUIC.PCUICAst]
map_decl_id_spec_cond [in MetaRocq.PCUIC.PCUICAst]
map_decl_id_spec [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_eq_spec [in MetaRocq.PCUIC.PCUICAst]
map_predicate_eq_spec [in MetaRocq.PCUIC.PCUICAst]
map_predicate_id [in MetaRocq.PCUIC.PCUICAst]
map_predicate_map_predicate [in MetaRocq.PCUIC.PCUICAst]
map_k_bcontext [in MetaRocq.PCUIC.PCUICAst]
map_k_bbody [in MetaRocq.PCUIC.PCUICAst]
map_bcontext [in MetaRocq.PCUIC.PCUICAst]
map_bbody [in MetaRocq.PCUIC.PCUICAst]
map_k_puinst [in MetaRocq.PCUIC.PCUICAst]
map_k_pcontext [in MetaRocq.PCUIC.PCUICAst]
map_k_preturn [in MetaRocq.PCUIC.PCUICAst]
map_k_pparams [in MetaRocq.PCUIC.PCUICAst]
map_puinst [in MetaRocq.PCUIC.PCUICAst]
map_pcontext [in MetaRocq.PCUIC.PCUICAst]
map_preturn [in MetaRocq.PCUIC.PCUICAst]
map_pparams [in MetaRocq.PCUIC.PCUICAst]
map_remove_match_on_box_repeat_box [in MetaRocq.Erasure.EOptimizePropDiscr]
map_repeat [in MetaRocq.Erasure.EOptimizePropDiscr]
map_opt_length [in MetaRocq.Erasure.EReorderCstrs]
map_optimize_repeat_box [in MetaRocq.Erasure.EReorderCstrs]
map_depth_hom [in MetaRocq.PCUIC.Syntax.PCUICDepth]
map_All_length [in MetaRocq.Utils.All_Forall]
map_option_out_All [in MetaRocq.Utils.All_Forall]
map_option_Some [in MetaRocq.Utils.All_Forall]
map_eq_inj [in MetaRocq.Utils.All_Forall]
map_fix_subst [in MetaRocq.PCUIC.PCUICParallelReduction]
map_cofix_subst [in MetaRocq.PCUIC.PCUICParallelReduction]
map_trans_env [in MetaRocq.ErasurePlugin.ETransform]
map_In_length [in MetaRocq.ErasurePlugin.Erasure]
map_subst_let_expand_lift [in MetaRocq.PCUIC.PCUICInductives]
map_subst_let_expand_to_extended_list [in MetaRocq.PCUIC.PCUICInductives]
map_subst_let_expand_k_to_extended_list_lift [in MetaRocq.PCUIC.PCUICInductives]
map_subst_let_expand_k [in MetaRocq.PCUIC.PCUICInductives]
map_expand_lets_to_extended_list_k [in MetaRocq.PCUIC.PCUICInductives]
map_bcontext_redl [in MetaRocq.PCUIC.PCUICReduction]
map_inj [in MetaRocq.PCUIC.PCUICReduction]
map_decomp_recomp' [in MetaRocq.PCUIC.PCUICReduction]
map_decomp_recomp [in MetaRocq.PCUIC.PCUICReduction]
map_recomp_decomp' [in MetaRocq.PCUIC.PCUICReduction]
map_recomp_decomp [in MetaRocq.PCUIC.PCUICReduction]
map_subst_instance_to_extended_list_k [in MetaRocq.Template.UnivSubst]
map_fix_rho_rename [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix_subst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_cofix_subst' [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_cofix_subst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho_map [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_terms_map [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_brs_map [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_br_map [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fst_add_multiple [in MetaRocq.Erasure.EWcbvEvalNamed]
map_optimize_repeat_box [in MetaRocq.Erasure.EInlineProjections]
map_map2 [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_fold_context_k [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_option_out_check_one_cofix [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_option_out_check_one_fix [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_context_trans [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_map2 [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_array_model_set_type [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_array_model_set_default [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_array_model_set_value [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_vass_map_def_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_inst_idsn [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_strip_repeat_box [in MetaRocq.Erasure.ERemoveParams]
map_repeat [in MetaRocq.Erasure.ERemoveParams]
map_option_out_check_one_cofix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_option_out_check_one_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_map_comm [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_decl_subst_instance_set_binder_name [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_map2 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_branches_k_map_branches_k [in MetaRocq.Template.Ast]
map_branches_map_branches [in MetaRocq.Template.Ast]
map_branch_id_spec [in MetaRocq.Template.Ast]
map_branch_eq_spec [in MetaRocq.Template.Ast]
map_branch_id [in MetaRocq.Template.Ast]
map_branch_map_branch [in MetaRocq.Template.Ast]
map_bbody [in MetaRocq.Template.Ast]
map_k_puinst [in MetaRocq.Template.Ast]
map_k_pcontext [in MetaRocq.Template.Ast]
map_k_preturn [in MetaRocq.Template.Ast]
map_k_pparams [in MetaRocq.Template.Ast]
map_predicate_id_spec [in MetaRocq.Template.Ast]
map_predicate_eq_spec [in MetaRocq.Template.Ast]
map_predicate_id [in MetaRocq.Template.Ast]
map_predicate_map_predicate [in MetaRocq.Template.Ast]
map_puints [in MetaRocq.Template.Ast]
map_preturn [in MetaRocq.Template.Ast]
map_pparams [in MetaRocq.Template.Ast]
map_primIn_spec [in MetaRocq.Erasure.EPrimitive]
map_prim_eq_prop [in MetaRocq.Erasure.EPrimitive]
map_prim_eq [in MetaRocq.Erasure.EPrimitive]
map_prim_id_prop [in MetaRocq.Erasure.EPrimitive]
map_prim_id [in MetaRocq.Erasure.EPrimitive]
map_prim_compose [in MetaRocq.Erasure.EPrimitive]
map_lift_map_lift [in MetaRocq.PCUIC.PCUICCasesHelper]
map_non_nil [in MetaRocq.Erasure.ELiftSubst]
map_def_id_spec [in MetaRocq.Erasure.ELiftSubst]
map_def_eq_spec [in MetaRocq.Erasure.ELiftSubst]
map_trans_repeat_box [in MetaRocq.Erasure.ECoInductiveToInductive]
map_repeat [in MetaRocq.Erasure.ECoInductiveToInductive]
map2i_ext [in MetaRocq.Utils.MRList]
map2_set_binder_name_expand_lets [in MetaRocq.PCUIC.PCUICSR]
map2_ext [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map2_map_left [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map2_map [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map2_snd [in MetaRocq.Utils.MRList]
map2_diag [in MetaRocq.Utils.MRList]
map2_map_l [in MetaRocq.Utils.MRList]
map2_length [in MetaRocq.Utils.MRList]
map2_mapi [in MetaRocq.Utils.MRList]
map2_ext [in MetaRocq.Utils.MRList]
map2_map2_bias_left [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2_bias_left_length [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_set_binder_name_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_map_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_set_binder_name_fold [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
map2_set_binder_name_alpha_eq [in MetaRocq.PCUIC.PCUICContexts]
map2_set_binder_name_alpha [in MetaRocq.PCUIC.PCUICContexts]
map2_set_binder_name_alpha_eq [in MetaRocq.PCUIC.PCUICCasesContexts]
map2_app [in MetaRocq.Utils.All_Forall]
map2_set_binder_name_map [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map2_map_r [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map2_set_binder_name_context_assumptions [in MetaRocq.PCUIC.Syntax.PCUICCases]
map2_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
map2_trans [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_map_map [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_alpha_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_alpha [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_cst [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2_set_binder_name_context_assumptions [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2_trans [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2_map_map [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
masked_weakening [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_all_zeros [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_map [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_app [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_length [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_len [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_count_zeros [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_nil [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
mask_rev [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
mask_last [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
meta_conv_all [in MetaRocq.PCUIC.PCUICTyping]
meta_conv_term [in MetaRocq.PCUIC.PCUICTyping]
meta_conv [in MetaRocq.PCUIC.PCUICTyping]
mfixpoint_depth_nth_error [in MetaRocq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth_In [in MetaRocq.PCUIC.Syntax.PCUICDepth]
mkAppBox_repeat [in MetaRocq.Erasure.Prelim]
mkAppMkApps [in MetaRocq.Template.AstUtils]
mkApps_snoc [in MetaRocq.PCUIC.PCUICNormal]
mkApps_snoc [in MetaRocq.Erasure.Prelim]
mkApps_tsize [in MetaRocq.Examples.tauto]
mkApps_tApp [in MetaRocq.SafeChecker.PCUICSafeReduce]
mkApps_Prim_nil [in MetaRocq.PCUIC.PCUICSafeLemmata]
mkApps_Prod_nil [in MetaRocq.PCUIC.PCUICSafeLemmata]
mkApps_app [in MetaRocq.Template.AstUtils]
mkApps_nisApp [in MetaRocq.Template.AstUtils]
mkApps_tApp [in MetaRocq.Template.AstUtils]
mkApps_eq_inj [in MetaRocq.Template.AstUtils]
mkApps_mkApp [in MetaRocq.Template.AstUtils]
mkApps_nonempty [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_nisApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_elim [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_elim_rec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_decompose [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_decompose_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_inj [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_right [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_left [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_inv [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_head [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_Fix_spec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_notApp_inj [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_nApp_inj [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_inj [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_discr [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_tApp_inj [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_tApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_tRel [in MetaRocq.Template.EtaExpand]
mkApps_trans_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
mkApps_ex [in MetaRocq.Template.LiftSubst]
mkApps_tRel [in MetaRocq.Template.LiftSubst]
mkApps_tApp [in MetaRocq.Template.LiftSubst]
mkApps_ind_typing_spine [in MetaRocq.PCUIC.PCUICInductiveInversion]
mkApps_context_hole [in MetaRocq.PCUIC.PCUICReduction]
mkApps_tApp [in MetaRocq.Template.TypingWf]
mkApps_tApp' [in MetaRocq.Template.TypingWf]
mkApps_trans_wf [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
mkApps_app [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
mkApps_morphism [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
mkApps_eq [in MetaRocq.Erasure.EAstUtils]
mkApps_elim [in MetaRocq.Erasure.EAstUtils]
mkApps_elim_rec [in MetaRocq.Erasure.EAstUtils]
mkApps_eq_right [in MetaRocq.Erasure.EAstUtils]
mkApps_head_inj [in MetaRocq.Erasure.EAstUtils]
mkApps_eq_inj [in MetaRocq.Erasure.EAstUtils]
mkApps_eq_decompose_app_rec [in MetaRocq.Erasure.EAstUtils]
mkApps_head_spine_decompose [in MetaRocq.Erasure.EAstUtils]
mkApps_head_spine [in MetaRocq.Erasure.EAstUtils]
mkApps_app [in MetaRocq.Erasure.EAstUtils]
mkApp_tsize [in MetaRocq.Examples.tauto]
mkApp_tApp [in MetaRocq.Template.AstUtils]
mkApp_mkApps [in MetaRocq.Template.AstUtils]
mkApp_mkApps [in MetaRocq.Template.TypingWf]
mkApp_ex [in MetaRocq.Template.TypingWf]
mkApp_ex_wf [in MetaRocq.Template.TypingWf]
mkAssumArity_it_mkProd_or_LetIn [in MetaRocq.SafeChecker.PCUICSafeReduce]
mk_ctx_subst_length [in MetaRocq.PCUIC.PCUICContextSubst]
mk_ctx_subst_spec [in MetaRocq.PCUIC.PCUICContextSubst]
mk_ctx_subst_spec' [in MetaRocq.PCUIC.PCUICSpine]
ModPathComp.compare_trans [in MetaRocq.Common.Kernames]
ModPathComp.compare_sym [in MetaRocq.Common.Kernames]
ModPathComp.compare_eq [in MetaRocq.Common.Kernames]
ModPathComp.nat_compare_trans [in MetaRocq.Common.Kernames]
ModPathComp.nat_compare_sym [in MetaRocq.Common.Kernames]
monad_map_app_invs [in MetaRocq.SafeChecker.PCUICErrors]
monad_map_app [in MetaRocq.SafeChecker.PCUICErrors]
monad_length_map [in MetaRocq.SafeChecker.PCUICErrors]
monad_map_Forall2 [in MetaRocq.SafeChecker.PCUICErrors]
monad_map_All2 [in MetaRocq.SafeChecker.PCUICErrors]
monomorphic_level_in_global_ext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_level_notin_levels_of_udecl [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_global_constraint_ext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_global_constraint [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_level_notin_AUContext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
MSetAVL.LtIrrel.Raw.bst_irrel [in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.gt_tree_irrel [in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.lt_tree_irrel [in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.above_spec [in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.below_spec [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.Exists_alt_iff [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_forall2_iff [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_forall_iff [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_alt_iff [in MetaRocq.Utils.MRMSets]
| 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) |