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