| 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 (definition)
make_wf_env_ext [in MetaCoq.SafeChecker.PCUICWfEnvImpl]make_wf_env_ext [in MetaCoq.Examples.typing_correctness]
make_graph [in MetaCoq.Template.common.uGraph]
make_fresh_name [in MetaCoq.SafeChecker.PCUICConsistency]
make_context_subst [in MetaCoq.PCUIC.PCUICContextSubst]
make_abstract_env_ext [in MetaCoq.SafeChecker.PCUICSafeChecker]
make_wf_env_ext [in MetaCoq.Examples.metacoq_tour_prelude]
make_inductive_body [in MetaCoq.Template.AstUtils]
make_constructor_body [in MetaCoq.Template.AstUtils]
mapi [in MetaCoq.Template.utils.MCList]
mapi_context_In [in MetaCoq.Template.BasicAst]
mapi_context [in MetaCoq.Template.BasicAst]
mapi_rec [in MetaCoq.Template.utils.MCList]
mapopt [in MetaCoq.Template.monad_utils]
map_decl_body [in MetaCoq.Template.EtaExpand]
map_context [in MetaCoq.Template.BasicAst]
map_decl [in MetaCoq.Template.BasicAst]
map_def [in MetaCoq.Template.BasicAst]
map_binder_annot [in MetaCoq.Template.BasicAst]
map_InP [in MetaCoq.PCUIC.utils.PCUICAstUtils]
map_All [in MetaCoq.Template.utils.All_Forall]
map_InP [in MetaCoq.Template.utils.MCList]
map_In [in MetaCoq.Template.utils.MCList]
map_decl_na [in MetaCoq.PCUIC.utils.PCUICOnOne]
map_branches [in MetaCoq.Template.Ast]
map_branch [in MetaCoq.Template.Ast]
map_predicate_k [in MetaCoq.Template.Ast]
map_predicate [in MetaCoq.Template.Ast]
map_branch_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_typing_result [in MetaCoq.SafeChecker.PCUICSafeRetyping]
map_trans_minductive_body [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_one_ind_body [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_constructor_body [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_branch_k [in MetaCoq.PCUIC.PCUICAst]
map_branches [in MetaCoq.PCUIC.PCUICAst]
map_branch [in MetaCoq.PCUIC.PCUICAst]
map_predicate_k [in MetaCoq.PCUIC.PCUICAst]
map_predicate [in MetaCoq.PCUIC.PCUICAst]
map_erase [in MetaCoq.Erasure.ErasureFunction]
map_context [in MetaCoq.Erasure.EAst]
map_decl [in MetaCoq.Erasure.EAst]
map_def [in MetaCoq.Erasure.EAst]
map_constr_with_binders [in MetaCoq.Template.Checker]
map_case_branch_with_binders [in MetaCoq.Template.Checker]
map_predicate_with_binders [in MetaCoq.Template.Checker]
map_context_with_binders [in MetaCoq.Template.Checker]
map_option_out [in MetaCoq.Template.utils.MCOption]
map_pair [in MetaCoq.Template.utils.MCProd]
map_mutual_inductive_body' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_one_inductive_body' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_constructor_body' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_fix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_brs_wf [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_br_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_br_wf [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_terms [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_decl_anon [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
map_def_anon [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
map2 [in MetaCoq.Template.utils.MCList]
map2i [in MetaCoq.Template.utils.MCList]
map2i_rec [in MetaCoq.Template.utils.MCList]
map2_bias_left [in MetaCoq.PCUIC.TemplateToPCUIC]
max_name_length [in MetaCoq.SafeChecker.PCUICConsistency]
maybe_string_of_list [in MetaCoq.Erasure.EAstUtils]
mFix [in MetaCoq.SafeChecker.PCUICSafeConversion]
mFixMfixMismatch [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfixpoint [in MetaCoq.Template.BasicAst]
mfixpoint [in MetaCoq.Erasure.EAst]
mfixpoint_size [in MetaCoq.Examples.tauto]
mfixpoint_size [in MetaCoq.PCUIC.utils.PCUICSize]
mfixpoint_depth_gen [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mFixRargMismatch [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix_hole_context [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mFix_mfix [in MetaCoq.SafeChecker.PCUICSafeConversion]
mind_body_to_entry [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mind_body_to_entry [in MetaCoq.Template.AstUtils]
mkApp [in MetaCoq.Template.Ast]
mkApp [in MetaCoq.Erasure.EAst]
mkAppBox [in MetaCoq.Erasure.Extract]
mkApps [in MetaCoq.Template.Ast]
mkApps [in MetaCoq.PCUIC.PCUICAst]
mkApps [in MetaCoq.Erasure.EAst]
MkAppsInd.case [in MetaCoq.Erasure.EInduction]
MkAppsInd.inspect [in MetaCoq.Erasure.EInduction]
MkAppsInd.rec [in MetaCoq.Erasure.EInduction]
mkApps_decompose_app [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app_rec [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app [in MetaCoq.PCUIC.Syntax.PCUICInduction]
mkApps_decompose_app_rec [in MetaCoq.PCUIC.Syntax.PCUICInduction]
mkApps_context [in MetaCoq.PCUIC.PCUICReduction]
mkAssumArity [in MetaCoq.SafeChecker.PCUICSafeReduce]
mkCase_old [in MetaCoq.Template.AstUtils]
mkImpl [in MetaCoq.Examples.demo]
mk_env_flags [in MetaCoq.Erasure.EWcbvEval]
ModPathComp.compare [in MetaCoq.Template.Kernames]
ModPathComp.eq [in MetaCoq.Template.Kernames]
ModPathComp.eq_univ [in MetaCoq.Template.Kernames]
ModPathComp.mpbound_compare [in MetaCoq.Template.Kernames]
ModPathComp.t [in MetaCoq.Template.Kernames]
modpath_eq_dec [in MetaCoq.Template.Kernames]
monad_All_All [in MetaCoq.Template.monad_utils]
monad_Alli_nth [in MetaCoq.Template.monad_utils]
monad_Alli_nth_gen [in MetaCoq.Template.monad_utils]
monad_Alli_All [in MetaCoq.Template.monad_utils]
monad_Alli [in MetaCoq.Template.monad_utils]
monad_prod [in MetaCoq.Template.monad_utils]
monad_All2 [in MetaCoq.Template.monad_utils]
monad_All [in MetaCoq.Template.monad_utils]
monad_iter [in MetaCoq.Template.monad_utils]
monad_map2 [in MetaCoq.Template.monad_utils]
monad_map_i [in MetaCoq.Template.monad_utils]
monad_map_i_aux [in MetaCoq.Template.monad_utils]
monad_fold_right [in MetaCoq.Template.monad_utils]
monad_fold_left [in MetaCoq.Template.monad_utils]
monad_map [in MetaCoq.Template.monad_utils]
monad_Alli_nth_forall [in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_Alli_nth_gen_forall [in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_lift_ext [in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_All_All [in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_mapi [in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_mapi_rec [in MetaCoq.SafeChecker.PCUICSafeChecker]
monomorph_globref_term [in MetaCoq.Translations.translation_utils]
moveL_moveR_transport_V [in MetaCoq.Translations.MiniHoTT]
moveL_moveR_transport_p [in MetaCoq.Translations.MiniHoTT]
moveL_equiv_V [in MetaCoq.Translations.MiniHoTT]
moveL_equiv_M [in MetaCoq.Translations.MiniHoTT]
moveL_transport_V_1 [in MetaCoq.Translations.MiniHoTT]
moveL_transport_p_V [in MetaCoq.Translations.MiniHoTT]
moveL_transport_V_V [in MetaCoq.Translations.MiniHoTT]
moveL_transport_p [in MetaCoq.Translations.MiniHoTT]
moveL_transport_V [in MetaCoq.Translations.MiniHoTT]
moveL_V1 [in MetaCoq.Translations.MiniHoTT]
moveL_1V [in MetaCoq.Translations.MiniHoTT]
moveL_M1 [in MetaCoq.Translations.MiniHoTT]
moveL_1M [in MetaCoq.Translations.MiniHoTT]
moveL_pV [in MetaCoq.Translations.MiniHoTT]
moveL_Vp [in MetaCoq.Translations.MiniHoTT]
moveL_pM [in MetaCoq.Translations.MiniHoTT]
moveL_Mp [in MetaCoq.Translations.MiniHoTT]
moveL_moveR_transport_V [in MetaCoq.Translations.MiniHoTT_paths]
moveL_moveR_transport_p [in MetaCoq.Translations.MiniHoTT_paths]
moveL_equiv_V [in MetaCoq.Translations.MiniHoTT_paths]
moveL_equiv_M [in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_V_1 [in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_p_V [in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_V_V [in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_p [in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_V [in MetaCoq.Translations.MiniHoTT_paths]
moveL_V1 [in MetaCoq.Translations.MiniHoTT_paths]
moveL_1V [in MetaCoq.Translations.MiniHoTT_paths]
moveL_M1 [in MetaCoq.Translations.MiniHoTT_paths]
moveL_1M [in MetaCoq.Translations.MiniHoTT_paths]
moveL_pV [in MetaCoq.Translations.MiniHoTT_paths]
moveL_Vp [in MetaCoq.Translations.MiniHoTT_paths]
moveL_pM [in MetaCoq.Translations.MiniHoTT_paths]
moveL_Mp [in MetaCoq.Translations.MiniHoTT_paths]
moveR_moveL_transport_p [in MetaCoq.Translations.MiniHoTT]
moveR_moveL_transport_V [in MetaCoq.Translations.MiniHoTT]
moveR_equiv_V [in MetaCoq.Translations.MiniHoTT]
moveR_equiv_M [in MetaCoq.Translations.MiniHoTT]
moveR_transport_V_V [in MetaCoq.Translations.MiniHoTT]
moveR_transport_p_V [in MetaCoq.Translations.MiniHoTT]
moveR_transport_V [in MetaCoq.Translations.MiniHoTT]
moveR_transport_p [in MetaCoq.Translations.MiniHoTT]
moveR_V1 [in MetaCoq.Translations.MiniHoTT]
moveR_1V [in MetaCoq.Translations.MiniHoTT]
moveR_1M [in MetaCoq.Translations.MiniHoTT]
moveR_M1 [in MetaCoq.Translations.MiniHoTT]
moveR_pV [in MetaCoq.Translations.MiniHoTT]
moveR_Vp [in MetaCoq.Translations.MiniHoTT]
moveR_pM [in MetaCoq.Translations.MiniHoTT]
moveR_Mp [in MetaCoq.Translations.MiniHoTT]
moveR_moveL_transport_p [in MetaCoq.Translations.MiniHoTT_paths]
moveR_moveL_transport_V [in MetaCoq.Translations.MiniHoTT_paths]
moveR_equiv_V [in MetaCoq.Translations.MiniHoTT_paths]
moveR_equiv_M [in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_V_V [in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_p_V [in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_V [in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_p [in MetaCoq.Translations.MiniHoTT_paths]
moveR_V1 [in MetaCoq.Translations.MiniHoTT_paths]
moveR_1V [in MetaCoq.Translations.MiniHoTT_paths]
moveR_1M [in MetaCoq.Translations.MiniHoTT_paths]
moveR_M1 [in MetaCoq.Translations.MiniHoTT_paths]
moveR_pV [in MetaCoq.Translations.MiniHoTT_paths]
moveR_Vp [in MetaCoq.Translations.MiniHoTT_paths]
moveR_pM [in MetaCoq.Translations.MiniHoTT_paths]
moveR_Mp [in MetaCoq.Translations.MiniHoTT_paths]
move_ws_term [in MetaCoq.PCUIC.PCUICConfluence]
Msem [in MetaCoq.Examples.tauto]
mut_pt_i [in MetaCoq.Examples.demo]
mut_list_i [in MetaCoq.Examples.demo]
mut_i [in MetaCoq.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 | (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) |