| 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 (definition)
make_context_subst [in MetaRocq.PCUIC.PCUICContextSubst]make_template_program_env [in MetaRocq.Template.TemplateProgram]
make_wf_env_ext [in MetaRocq.Examples.typing_correctness]
make_inductive_body [in MetaRocq.Template.AstUtils]
make_constructor_body [in MetaRocq.Template.AstUtils]
make_quotation_of [in MetaRocq.Quotation.ToPCUIC.Init]
make_env [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
make_abstract_env_ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
make_quotation_of [in MetaRocq.Quotation.ToTemplate.Init]
make_All_All [in MetaRocq.Utils.All_Forall]
make_All [in MetaRocq.Utils.All_Forall]
make_unsafe_passes [in MetaRocq.ErasurePlugin.Erasure]
make_wf_env_ext [in MetaRocq.Examples.metarocq_tour_prelude]
make_graph [in MetaRocq.Common.uGraph]
make_All [in MetaRocq.SafeChecker.PCUICTypeChecker]
make_case [in MetaRocq.PCUIC.PCUICCasesHelper]
make_br [in MetaRocq.PCUIC.PCUICCasesHelper]
make_case_pred [in MetaRocq.PCUIC.PCUICCasesHelper]
make_wf_env_ext [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
mapi [in MetaRocq.Utils.MRList]
mapi_rec [in MetaRocq.Utils.MRList]
mapi_length_transparent [in MetaRocq.Erasure.Typed.TypeAnnotations]
mapi_context_In [in MetaRocq.Common.BasicAst]
mapi_context [in MetaRocq.Common.BasicAst]
mapopt [in MetaRocq.Utils.monad_utils]
mapu_prim [in MetaRocq.PCUIC.utils.PCUICPrimitive]
mapu_array_model [in MetaRocq.PCUIC.utils.PCUICPrimitive]
map_annots [in MetaRocq.Erasure.Typed.Annotations]
map_annot [in MetaRocq.Erasure.Typed.Annotations]
map_InP [in MetaRocq.Utils.MRList]
map_In [in MetaRocq.Utils.MRList]
map_termM [in MetaRocq.Template.AstUtils]
map_term [in MetaRocq.Template.AstUtils]
map_term_with_bindersM [in MetaRocq.Template.AstUtils]
map_branch_with_bindersM [in MetaRocq.Template.AstUtils]
map_predicate_with_bindersM [in MetaRocq.Template.AstUtils]
map_defM [in MetaRocq.Template.AstUtils]
map_term_with_binders [in MetaRocq.Template.AstUtils]
map_branch_with_binders [in MetaRocq.Template.AstUtils]
map_predicate_with_binders [in MetaRocq.Template.AstUtils]
map_decl_na [in MetaRocq.PCUIC.utils.PCUICOnOne]
map_subterms [in MetaRocq.Erasure.Typed.Optimize]
map_typing_result [in MetaRocq.SafeChecker.PCUICSafeRetyping]
map_InP [in MetaRocq.PCUIC.utils.PCUICAstUtils]
map_decl_body [in MetaRocq.Template.EtaExpand]
map_trans_minductive_body [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_one_ind_body [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_constructor_body [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_onPrim [in MetaRocq.PCUIC.PCUICEtaExpand]
map_All [in MetaRocq.PCUIC.PCUICEtaExpand]
map_subterms [in MetaRocq.Erasure.Typed.Utils]
map_with_bigprod [in MetaRocq.Erasure.Typed.Utils]
map_In [in MetaRocq.Erasure.Typed.Utils]
map_snd [in MetaRocq.Erasure.Typed.Utils]
map_fst [in MetaRocq.Erasure.Typed.Utils]
map_decl_anon [in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
map_def_anon [in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
map_option_out [in MetaRocq.Utils.MROption]
map_branch_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_error [in MetaRocq.Erasure.Typed.ResultMonad]
map_context [in MetaRocq.Common.BasicAst]
map_decl [in MetaRocq.Common.BasicAst]
map_def [in MetaRocq.Common.BasicAst]
map_binder_annot [in MetaRocq.Common.BasicAst]
map_subterms [in MetaRocq.Erasure.EBeta]
map_branch_k [in MetaRocq.PCUIC.PCUICAst]
map_branches [in MetaRocq.PCUIC.PCUICAst]
map_branch [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k [in MetaRocq.PCUIC.PCUICAst]
map_predicate [in MetaRocq.PCUIC.PCUICAst]
map_All2 [in MetaRocq.Utils.All_Forall]
map_All [in MetaRocq.Utils.All_Forall]
map_of_typed_global_env [in MetaRocq.ErasurePlugin.ETransform]
map_eval_primitive [in MetaRocq.Erasure.EWcbvEval]
map_constr_with_binders [in MetaRocq.Template.Checker]
map_case_branch_with_binders [in MetaRocq.Template.Checker]
map_predicate_with_binders [in MetaRocq.Template.Checker]
map_context_with_binders [in MetaRocq.Template.Checker]
map_global_env_decls [in MetaRocq.Erasure.Typed.Certifying]
map_constants_global_env [in MetaRocq.Erasure.Typed.Certifying]
map_constants_global_decls [in MetaRocq.Erasure.Typed.Certifying]
map_context [in MetaRocq.Erasure.EAst]
map_decl [in MetaRocq.Erasure.EAst]
map_def [in MetaRocq.Erasure.EAst]
map_fix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_prim_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_brs_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_br_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_br_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_terms [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_pair [in MetaRocq.Utils.MRProd]
map_def_name [in MetaRocq.Erasure.EWcbvEvalNamed]
map_mutual_inductive_body' [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_one_inductive_body' [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_constructor_body' [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_branches [in MetaRocq.Template.Ast]
map_branch [in MetaRocq.Template.Ast]
map_predicate_k [in MetaRocq.Template.Ast]
map_predicate [in MetaRocq.Template.Ast]
map_onPrims [in MetaRocq.Erasure.EPrimitive]
map_All2_dep [in MetaRocq.Erasure.EPrimitive]
map_primIn [in MetaRocq.Erasure.EPrimitive]
map_prim [in MetaRocq.Erasure.EPrimitive]
map_array_model [in MetaRocq.Erasure.EPrimitive]
map2 [in MetaRocq.Utils.MRList]
map2i [in MetaRocq.Utils.MRList]
map2i_rec [in MetaRocq.Utils.MRList]
map2_bias_left [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
masked [in MetaRocq.Erasure.Typed.Optimize]
maybe_string_of_list [in MetaRocq.Erasure.EAstUtils]
mFix [in MetaRocq.SafeChecker.PCUICSafeConversion]
mFixMfixMismatch [in MetaRocq.SafeChecker.PCUICSafeConversion]
mfixpoint [in MetaRocq.Common.BasicAst]
mfixpoint [in MetaRocq.Erasure.EAst]
mfixpoint_size [in MetaRocq.Examples.tauto]
mfixpoint_size [in MetaRocq.PCUIC.utils.PCUICSize]
mfixpoint_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
mFixRargMismatch [in MetaRocq.SafeChecker.PCUICSafeConversion]
mfix_hole_context [in MetaRocq.PCUIC.Syntax.PCUICPosition]
mfix_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
mFix_mfix [in MetaRocq.SafeChecker.PCUICSafeConversion]
mind_body_to_entry [in MetaRocq.Template.AstUtils]
mind_body_to_entry [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApp [in MetaRocq.Erasure.EAst]
mkApp [in MetaRocq.Template.Ast]
mkAppBox [in MetaRocq.Erasure.Extract]
mkApps [in MetaRocq.PCUIC.PCUICAst]
mkApps [in MetaRocq.Erasure.EAst]
mkApps [in MetaRocq.Template.Ast]
MkAppsInd.case [in MetaRocq.Erasure.EInduction]
MkAppsInd.inspect [in MetaRocq.Erasure.EInduction]
MkAppsInd.rec [in MetaRocq.Erasure.EInduction]
mkApps_spec_sind [in MetaRocq.Template.AstUtils]
mkApps_spec_rec [in MetaRocq.Template.AstUtils]
mkApps_spec_ind [in MetaRocq.Template.AstUtils]
mkApps_spec_rect [in MetaRocq.Template.AstUtils]
mkApps_spec_sind [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_rec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_ind [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_rect [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app_rec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app [in MetaRocq.PCUIC.Syntax.PCUICInduction]
mkApps_decompose_app_rec [in MetaRocq.PCUIC.Syntax.PCUICInduction]
mkApps_context [in MetaRocq.PCUIC.PCUICReduction]
mkApps_spec_sind [in MetaRocq.Erasure.EAstUtils]
mkApps_spec_rec [in MetaRocq.Erasure.EAstUtils]
mkApps_spec_ind [in MetaRocq.Erasure.EAstUtils]
mkApps_spec_rect [in MetaRocq.Erasure.EAstUtils]
mkAssumArity [in MetaRocq.SafeChecker.PCUICSafeReduce]
mkCase_old [in MetaRocq.Template.AstUtils]
mkImpl [in MetaRocq.Examples.demo]
mkLambda_or_LetIn [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
mkNormalArity [in MetaRocq.Erasure.Typed.Erasure]
mkTApps [in MetaRocq.Erasure.Typed.ExAst]
mk_ctx_subst [in MetaRocq.PCUIC.PCUICContextSubst]
mk_env_flags [in MetaRocq.Erasure.EWcbvEval]
ModPathComp.compare [in MetaRocq.Common.Kernames]
ModPathComp.eq [in MetaRocq.Common.Kernames]
ModPathComp.eq_univ [in MetaRocq.Common.Kernames]
ModPathComp.mpbound_compare [in MetaRocq.Common.Kernames]
ModPathComp.t [in MetaRocq.Common.Kernames]
modpath_is_okay [in MetaRocq.Quotation.CommonUtils]
modpath_is_absolute [in MetaRocq.Quotation.CommonUtils]
modpath_eq_dec [in MetaRocq.Common.Kernames]
modpath_sind [in MetaRocq.Common.Kernames]
modpath_rec [in MetaRocq.Common.Kernames]
modpath_ind [in MetaRocq.Common.Kernames]
modpath_rect [in MetaRocq.Common.Kernames]
monad_map_branches_k [in MetaRocq.Template.MonadAst]
monad_map_branches [in MetaRocq.Template.MonadAst]
monad_map_branch [in MetaRocq.Template.MonadAst]
monad_map_predicate_k [in MetaRocq.Template.MonadAst]
monad_map_predicate [in MetaRocq.Template.MonadAst]
monad_map_branches_k [in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_branch_k [in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_branches [in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_branch [in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_predicate_k [in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_predicate [in MetaRocq.PCUIC.PCUICMonadAst]
monad_trans_global_decl [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_minductive_body [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constant_body [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_one_ind_body [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_projection_body [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constructor_body [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_local [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_decl [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_global_decl' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_minductive_body' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constant_body' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_one_ind_body' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_projection_body' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constructor_body' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_local' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_decl' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_map_In [in MetaRocq.Erasure.Typed.Utils]
monad_All_All [in MetaRocq.Utils.monad_utils]
monad_Alli_nth [in MetaRocq.Utils.monad_utils]
monad_Alli_nth_gen [in MetaRocq.Utils.monad_utils]
monad_Alli_All [in MetaRocq.Utils.monad_utils]
monad_Alli [in MetaRocq.Utils.monad_utils]
monad_prod [in MetaRocq.Utils.monad_utils]
monad_All2 [in MetaRocq.Utils.monad_utils]
monad_All [in MetaRocq.Utils.monad_utils]
monad_iter [in MetaRocq.Utils.monad_utils]
monad_map2 [in MetaRocq.Utils.monad_utils]
monad_map_i [in MetaRocq.Utils.monad_utils]
monad_map_i_aux [in MetaRocq.Utils.monad_utils]
monad_fold_right [in MetaRocq.Utils.monad_utils]
monad_fold_left [in MetaRocq.Utils.monad_utils]
monad_option_map [in MetaRocq.Utils.monad_utils]
monad_map [in MetaRocq.Utils.monad_utils]
monad_Alli_nth_forall [in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_Alli_nth_gen_forall [in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_lift_ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_All_All [in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_mapi [in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_mapi_rec [in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_fold_context [in MetaRocq.Common.MonadBasicAst]
monad_fold_context_In [in MetaRocq.Common.MonadBasicAst]
monad_mapi_context_In [in MetaRocq.Common.MonadBasicAst]
monad_fold_context_k [in MetaRocq.Common.MonadBasicAst]
monad_mapi_context [in MetaRocq.Common.MonadBasicAst]
monad_map_context [in MetaRocq.Common.MonadBasicAst]
monad_map_decl [in MetaRocq.Common.MonadBasicAst]
monad_typ_or_sort_map [in MetaRocq.Common.MonadBasicAst]
monad_map_def [in MetaRocq.Common.MonadBasicAst]
monad_map_binder_annot [in MetaRocq.Common.MonadBasicAst]
move_ws_term [in MetaRocq.PCUIC.PCUICConfluence]
Msem [in MetaRocq.Examples.tauto]
MSetAVL.DecideWithLeibniz.Raw.tree_dec [in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.t_dec [in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw.bst_dec [in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw.gt_tree_dec [in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw.lt_tree_dec [in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.invert_bst [in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.above [in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.below [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.Exists_dec [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.Exists_alt [in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_alt [in MetaRocq.Utils.MRMSets]
mut_pt_i [in MetaRocq.Examples.demo]
mut_list_i [in MetaRocq.Examples.demo]
mut_i [in MetaRocq.Examples.demo]
| 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) |