| 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) |
L (lemma)
lambdabox_pres_fo [in MetaRocq.ErasurePlugin.ErasureCorrectness]Lambda_conv_cum_inv [in MetaRocq.PCUIC.PCUICConversion]
last_nonempty_eq [in MetaRocq.Utils.MRList]
last_app [in MetaRocq.Utils.MRList]
last_inv [in MetaRocq.Utils.MRList]
laxest_checker_flags_laxest [in MetaRocq.Common.config]
leb_spect [in MetaRocq.PCUIC.PCUICFirstorder]
leb_spec_Set [in MetaRocq.Utils.MRArith]
leb_S [in MetaRocq.PCUIC.PCUICParallelReduction]
length_nil [in MetaRocq.Utils.MRList]
length_skipn_map [in MetaRocq.Utils.MRList]
length_skipn [in MetaRocq.Utils.MRList]
length_rev_map [in MetaRocq.Utils.MRList]
length_rev [in MetaRocq.Utils.MRList]
length_skipn_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
length_subst_context [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lenm_eq [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
leqb_term_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
leqb_univ_expr_n_spec_gen' [in MetaRocq.Common.uGraph]
leqb_universe_n_spec_gen [in MetaRocq.Common.uGraph]
leqb_universe_n_spec0_gen [in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec_gen [in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec0_gen [in MetaRocq.Common.uGraph]
leqb_expr_n_spec_gen [in MetaRocq.Common.uGraph]
leqb_expr_n_spec0_gen [in MetaRocq.Common.uGraph]
leqb_level_n_spec [in MetaRocq.Common.uGraph]
leq_term_mkApps [in MetaRocq.PCUIC.PCUICCumulativity]
leq_term_App [in MetaRocq.PCUIC.PCUICCumulativity]
leq_term_leq_term_napp [in MetaRocq.PCUIC.PCUICCumulativity]
leq_term_leq_term_napp [in MetaRocq.PCUIC.PCUICEquality]
leq_term_prop_sorted_r [in MetaRocq.PCUIC.PCUICElimination]
leq_term_prop_sorted_l [in MetaRocq.PCUIC.PCUICElimination]
leq_sort_propositional_l [in MetaRocq.PCUIC.PCUICElimination]
leq_prop_is_propositonal [in MetaRocq.Common.Universes]
leq_sort_prop_no_prop_sub_type [in MetaRocq.Common.Universes]
leq_sort_super [in MetaRocq.Common.Universes]
leq_sort_product_mon [in MetaRocq.Common.Universes]
leq_sort_config_impl [in MetaRocq.Common.Universes]
leq_universe_config_impl [in MetaRocq.Common.Universes]
leq_sort_subset [in MetaRocq.Common.Universes]
leq_sort_product [in MetaRocq.Common.Universes]
leq_sort_sup_r [in MetaRocq.Common.Universes]
leq_sort_sup_l [in MetaRocq.Common.Universes]
leq_csort_of_product_mon [in MetaRocq.Common.Universes]
leq_sort_leq_sort_n [in MetaRocq.Common.Universes]
leq_universe_subset [in MetaRocq.Common.Universes]
leq_universe_sup_mon [in MetaRocq.Common.Universes]
leq_universe_sup_r [in MetaRocq.Common.Universes]
leq_universe_sup_l [in MetaRocq.Common.Universes]
leq_sort_sort_of_products [in MetaRocq.PCUIC.PCUICSpine]
leq_term_subset [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
leq_term_App [in MetaRocq.Template.TermEquality]
leq_term_mkApps [in MetaRocq.Template.TermEquality]
leq_term_refl [in MetaRocq.Template.TermEquality]
leq_sortP_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
leq_universeP_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
leq_term_propositional_sorted_l [in MetaRocq.Erasure.ErasureFunctionProperties]
leq_sort_sort_of_products_mon [in MetaRocq.PCUIC.PCUICArities]
leq_term_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_sort_propositional_l [in MetaRocq.Erasure.EArities]
leq_sort_propositional_r [in MetaRocq.Erasure.EArities]
leq_term_propopositional_sorted_r [in MetaRocq.Erasure.EArities]
leq_term_propositional_sorted_l [in MetaRocq.Erasure.EArities]
leq_term_config_impl [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
leq_universe_vertices [in MetaRocq.Common.uGraph]
leq_universe_vertices1 [in MetaRocq.Common.uGraph]
leq_universe_vertices0 [in MetaRocq.Common.uGraph]
leq_term_empty_leq_term [in MetaRocq.PCUIC.PCUICPrincipality]
leq0_level_n_complete_gen [in MetaRocq.Common.uGraph]
LevelExprSet_For_all [in MetaRocq.PCUIC.PCUICCumulProp]
LevelExpr.val_make_npl [in MetaRocq.Common.Universes]
LevelExpr.val_make [in MetaRocq.Common.Universes]
LevelIn_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
LevelSetsUIP.ok_irrel [in MetaRocq.Common.Reflect]
LevelSet_union_empty [in MetaRocq.Common.Universes]
LevelSet_In_fold_right_add [in MetaRocq.Common.Universes]
LevelSet_pair_In [in MetaRocq.Common.Universes]
LevelSet_In_declare_and_uniquify_and_combine_levels_1_1 [in MetaRocq.Common.UniversesDec]
LevelSet_In_fold_add [in MetaRocq.Common.UniversesDec]
LevelSet_in_union_global [in MetaRocq.PCUIC.PCUICGlobalEnv]
levelset_for_all_eq [in MetaRocq.Common.uGraph]
levels_of_universe_spec [in MetaRocq.Common.UniversesDec]
levels_of_cscs_spec [in MetaRocq.Common.UniversesDec]
levels_of_cs2_spec [in MetaRocq.Common.UniversesDec]
levels_of_cs_spec [in MetaRocq.Common.UniversesDec]
levels_global_levels_declared [in MetaRocq.SafeChecker.PCUICSafeChecker]
levels_global_ext_constraint [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_global_constraint [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_univ_gc_declared_declared [in MetaRocq.Common.uGraph]
levels_gc_declared_declared [in MetaRocq.Common.uGraph]
level_var_instance_length [in MetaRocq.PCUIC.PCUICInductiveInversion]
level_gc_declared_declared [in MetaRocq.Common.uGraph]
Level.eqb_spec [in MetaRocq.Common.Universes]
le_irrel [in MetaRocq.PCUIC.PCUICWcbvEval]
liftP_ctx [in MetaRocq.PCUIC.Syntax.PCUICInduction]
liftP_ctx_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
lift_unlift_context [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift_term [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
lift_judgment_SR [in MetaRocq.PCUIC.PCUICSR]
lift_leq_term [in MetaRocq.PCUIC.PCUICEquality]
lift_eq_term [in MetaRocq.PCUIC.PCUICEquality]
lift_compare_context [in MetaRocq.PCUIC.PCUICEquality]
lift_compare_decls [in MetaRocq.PCUIC.PCUICEquality]
lift_compare_term [in MetaRocq.PCUIC.PCUICEquality]
lift_extended_subst' [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_extended_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkProd_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_app [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_alt [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_length [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_decl0 [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_to_extended_list_k [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_closed [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_mkApps [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_isApp [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_lt [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_ge [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_declared_constant [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
lift_context_add [in MetaRocq.PCUIC.Syntax.PCUICClosed]
lift_decl_closed [in MetaRocq.PCUIC.Syntax.PCUICClosed]
lift_to_extended_list_k [in MetaRocq.PCUIC.PCUICSpine]
lift_context0_app [in MetaRocq.PCUIC.PCUICSpine]
lift_context_subst_context [in MetaRocq.PCUIC.PCUICSpine]
lift_typing_wf_local [in MetaRocq.PCUIC.PCUICTyping]
lift_to_pred [in MetaRocq.PCUIC.PCUICConfluence]
lift_to_ws_red [in MetaRocq.PCUIC.PCUICConfluence]
lift_expand_lets_k [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
lift_wt_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
lift_sorting_lift_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
lift_to_extended_list_k [in MetaRocq.Template.LiftSubst]
lift_closed [in MetaRocq.Template.LiftSubst]
lift_mkApps [in MetaRocq.Template.LiftSubst]
lift_rel_lt [in MetaRocq.Template.LiftSubst]
lift_rel_ge [in MetaRocq.Template.LiftSubst]
lift_instance_length [in MetaRocq.PCUIC.PCUICInductiveInversion]
lift_isApp [in MetaRocq.Template.WfAst]
lift_to_wf_list [in MetaRocq.Template.WfAst]
lift_to_list [in MetaRocq.Template.WfAst]
lift_judgment_alpha [in MetaRocq.PCUIC.PCUICAlpha]
lift_renaming_0 [in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_rename [in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_renaming_0_rshift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_renaming_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_isLambda [in MetaRocq.Erasure.ESubstitution]
lift_inst_case_branch_context [in MetaRocq.Erasure.ESubstitution]
lift_iota_red [in MetaRocq.PCUIC.PCUICParallelReduction]
lift_rename' [in MetaRocq.PCUIC.PCUICParallelReduction]
lift_context_subst [in MetaRocq.PCUIC.PCUICInductives]
lift_context_expand_lets_ctx [in MetaRocq.PCUIC.PCUICInductives]
lift_context_subst_context_let_expand [in MetaRocq.PCUIC.PCUICInductives]
lift_context_lift_context [in MetaRocq.PCUIC.PCUICInductives]
lift_it_mkProd_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_fix_context [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_context_lift_context [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_typing2_wf_pred [in MetaRocq.Template.TypingWf]
lift_typing_wf_pred [in MetaRocq.Template.TypingWf]
lift_context_snoc [in MetaRocq.Template.TypingWf]
lift_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lift_dearg_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lift_dearg_single [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lift_wt_inv [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
lift_typing_is_open_term [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
lift_closed [in MetaRocq.Erasure.ELiftSubst]
lift_mkApps [in MetaRocq.Erasure.ELiftSubst]
lift_isApp [in MetaRocq.Erasure.ELiftSubst]
lift_rel_alt [in MetaRocq.Erasure.ELiftSubst]
lift_rel_lt [in MetaRocq.Erasure.ELiftSubst]
lift_rel_ge [in MetaRocq.Erasure.ELiftSubst]
lift0_context [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift0_p [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift0_id [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift0_open [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
lift0_p [in MetaRocq.Template.LiftSubst]
lift0_id [in MetaRocq.Template.LiftSubst]
lift0_rename [in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift0_inst_id [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
lift0_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
lift0_p [in MetaRocq.Erasure.ELiftSubst]
lift0_id [in MetaRocq.Erasure.ELiftSubst]
ListOrderedType.compare_trans [in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_lt_lt [in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_sym [in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_refl [in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_eq [in MetaRocq.Utils.MRCompare]
list_size_length [in MetaRocq.Examples.tauto]
list_size_map_hom [in MetaRocq.Utils.MRList]
list_size_map_le [in MetaRocq.Utils.MRList]
list_size_mapi_le [in MetaRocq.Utils.MRList]
list_size_mapi_rec_le [in MetaRocq.Utils.MRList]
list_size_map_eq [in MetaRocq.Utils.MRList]
list_size_mapi_eq [in MetaRocq.Utils.MRList]
list_size_mapi_rec_eq [in MetaRocq.Utils.MRList]
list_size_map [in MetaRocq.Utils.MRList]
list_size_length [in MetaRocq.Utils.MRList]
list_size_rev [in MetaRocq.Utils.MRList]
list_size_app [in MetaRocq.Utils.MRList]
list_rect_rev [in MetaRocq.Utils.MRList]
list_ind_rev [in MetaRocq.Utils.MRList]
list_size_skipn [in MetaRocq.Erasure.ErasureFunctionProperties]
list_length_ind [in MetaRocq.Template.LiftSubst]
list_length_rev_ind [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
list_size_rev [in MetaRocq.PCUIC.Syntax.PCUICInduction]
list_size_mapi_context_hom [in MetaRocq.PCUIC.Syntax.PCUICInduction]
list_depth_mapi_rec_le [in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_depth_rev [in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_depth_app [in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_map_swap_eq' [in MetaRocq.PCUIC.PCUICReduction]
list_map_swap_eq [in MetaRocq.PCUIC.PCUICReduction]
list_split_eq [in MetaRocq.PCUIC.PCUICReduction]
local_env_telescope [in MetaRocq.PCUIC.PCUICConfluence]
local_env_telescope [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
lookup_env_nlg [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
lookup_constructor_pars_args_implement_box [in MetaRocq.Erasure.EImplementBox]
lookup_inductive_implement_box [in MetaRocq.Erasure.EImplementBox]
lookup_constructor_implement_box [in MetaRocq.Erasure.EImplementBox]
lookup_env_implement_box [in MetaRocq.Erasure.EImplementBox]
lookup_constructor_pars_args_spec [in MetaRocq.Erasure.EImplementBox]
lookup_global_deps [in MetaRocq.Erasure.ErasureFunction]
lookup_env_In [in MetaRocq.Erasure.ErasureFunction]
lookup_env_Some_fresh [in MetaRocq.PCUIC.PCUICWeakeningEnv]
lookup_global_Some_fresh [in MetaRocq.PCUIC.PCUICWeakeningEnv]
lookup_projection_lookup_constructor [in MetaRocq.Erasure.ErasureProperties]
lookup_inductive_pars_unbox [in MetaRocq.Erasure.EUnboxing]
lookup_constructor_pars_args_unbox [in MetaRocq.Erasure.EUnboxing]
lookup_constructor_unbox [in MetaRocq.Erasure.EUnboxing]
lookup_env_unbox [in MetaRocq.Erasure.EUnboxing]
lookup_ind_decl_complete [in MetaRocq.SafeChecker.PCUICSafeRetyping]
lookup_env_cons_fresh [in MetaRocq.PCUIC.utils.PCUICAstUtils]
lookup_env_cons [in MetaRocq.PCUIC.utils.PCUICAstUtils]
lookup_env_nil [in MetaRocq.PCUIC.utils.PCUICAstUtils]
lookup_erase_global [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_global_app_wf [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_erase_decl [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_In_map_fst [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_erase_global_diff [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_erase_decl_None [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_cons_disc [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_ext [in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_global_extends [in MetaRocq.Template.EtaExpand]
lookup_env_Some_fresh [in MetaRocq.Template.EtaExpand]
lookup_global_Some_fresh [in MetaRocq.Template.EtaExpand]
lookup_global_map_on_snd [in MetaRocq.Template.EtaExpand]
lookup_lookup_global_env_None [in MetaRocq.Template.EtaExpand]
lookup_global_env_lookup [in MetaRocq.Template.EtaExpand]
lookup_lookup_global_env [in MetaRocq.Template.EtaExpand]
lookup_env_find [in MetaRocq.Erasure.Typed.WcbvEvalAux]
lookup_globals_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
lookup_projection_gen_transform [in MetaRocq.Erasure.EGenericGlobalMap]
lookup_constructor_gen_transform [in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_gen_transform [in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_gen_transform_env_None [in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_map_snd [in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_gen_transform_env_Some [in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_In [in MetaRocq.Erasure.EExtends]
lookup_constructor_pars_args_nopars [in MetaRocq.ErasurePlugin.ErasureCorrectness]
lookup_constructor_pars_args_lookup_inductive_pars [in MetaRocq.ErasurePlugin.ErasureCorrectness]
lookup_env_in_erase_global_deps [in MetaRocq.ErasurePlugin.ErasureCorrectness]
lookup_inductive_pars_constructor_pars_args [in MetaRocq.Erasure.EEtaExpandedFix]
lookup_global_In_wf [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
lookup_env_In [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
lookup_constructor_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_inductive_pars_optimize [in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_remove_match_on_box_env_None [in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_map_snd [in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_remove_match_on_box_env_Some [in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_projection_gen_transform [in MetaRocq.Erasure.EGenericMapEnv]
lookup_constructor_gen_transform [in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_gen_transform [in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_None [in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_map_snd [in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_Some [in MetaRocq.Erasure.EGenericMapEnv]
lookup_inductive_pars_optimize [in MetaRocq.Erasure.EReorderCstrs]
lookup_projection_reorder [in MetaRocq.Erasure.EReorderCstrs]
lookup_projection_ordinal [in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_reorder [in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc_None_reorder_one_ind [in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc_wf_tags [in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc_spec [in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_reorder [in MetaRocq.Erasure.EReorderCstrs]
lookup_constant_reorder [in MetaRocq.Erasure.EReorderCstrs]
lookup_env_reorder [in MetaRocq.Erasure.EReorderCstrs]
lookup_declared_constructor [in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_transform_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_inductive_transform_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_env_transform_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_constructor_pars_args_spec [in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_env_In_map_fst [in MetaRocq.ErasurePlugin.ETransform]
lookup_env_closed [in MetaRocq.Erasure.EWcbvEval]
lookup_inductive_map_on_snd_remove_decl [in MetaRocq.ErasurePlugin.Erasure]
lookup_inductive_erase_global_decls_deps [in MetaRocq.ErasurePlugin.Erasure]
lookup_lookup_global_env_None [in MetaRocq.ErasurePlugin.Erasure]
lookup_inductive_filter_deps_None [in MetaRocq.ErasurePlugin.Erasure]
lookup_inductive_filter_deps_Some [in MetaRocq.ErasurePlugin.Erasure]
lookup_env_filter_deps_None [in MetaRocq.ErasurePlugin.Erasure]
lookup_env_filter_deps [in MetaRocq.ErasurePlugin.Erasure]
lookup_env_filter [in MetaRocq.ErasurePlugin.Erasure]
lookup_in_env [in MetaRocq.Erasure.EWcbvEvalNamed]
lookup_annotate_env [in MetaRocq.Erasure.EWcbvEvalNamed]
lookup_env_wellformed [in MetaRocq.Erasure.EWellformed]
lookup_env_extends [in MetaRocq.Template.TypingWf]
lookup_projection_optimize [in MetaRocq.Erasure.EInlineProjections]
lookup_constructor_optimize [in MetaRocq.Erasure.EInlineProjections]
lookup_inductive_pars_optimize [in MetaRocq.Erasure.EInlineProjections]
lookup_env_optimize [in MetaRocq.Erasure.EInlineProjections]
lookup_env_optimize_env_None [in MetaRocq.Erasure.EInlineProjections]
lookup_env_map_snd [in MetaRocq.Erasure.EInlineProjections]
lookup_env_optimize_env_Some [in MetaRocq.Erasure.EInlineProjections]
lookup_inductive_wellformed [in MetaRocq.Erasure.EInlineProjections]
lookup_constructor_debox_types [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_debox_env_types [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_lookup_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_trans_env_inv [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_trans_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_dearg_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_Forall [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_trans_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_inductive_declared [in MetaRocq.PCUIC.Syntax.PCUICCases]
lookup_env_Some_fresh [in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor_pars_args_cstr_arity [in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor_lookup_inductive [in MetaRocq.Erasure.EGlobalEnv]
lookup_projection_lookup_constructor [in MetaRocq.Erasure.EGlobalEnv]
lookup_minductive_declared_inductive [in MetaRocq.Erasure.ERemoveParams]
lookup_minductive_declared_minductive [in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_spec [in MetaRocq.Erasure.ERemoveParams]
lookup_constructor_lookup_inductive_pars [in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_is_prop_and_pars [in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_strip [in MetaRocq.Erasure.ERemoveParams]
lookup_constructor_pars_args_strip [in MetaRocq.Erasure.ERemoveParams]
lookup_constructor_strip [in MetaRocq.Erasure.ERemoveParams]
lookup_env_strip [in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_constructor_pars_args [in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_None [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
lookup_lookup_env [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
lookup_constructor_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_trans_env_None [in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_map_snd [in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_trans_env_Some [in MetaRocq.Erasure.ECoInductiveToInductive]
Lookup.consistent_instance_length [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_ind_declared_constructors [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_projection_lookup_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constructor_lookup_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_inductive_lookup_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_minductive_lookup_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constant_lookup_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_levels_InSet [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_levels_memSet [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_levels_InSet [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_projection_declared_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constructor_declared_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_inductive_declared_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_minductive_declared_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constant_declared_gen [in MetaRocq.Common.EnvironmentTyping]
LSet_in_global_bounded [in MetaRocq.PCUIC.PCUICInductiveInversion]
LSet_in_poly_bounded [in MetaRocq.PCUIC.PCUICInductiveInversion]
lt_not_eq [in MetaRocq.Utils.ByteCompareSpec]
lt_trans [in MetaRocq.Utils.ByteCompareSpec]
lt_sort_irrefl [in MetaRocq.Common.Universes]
lt_level_irrel [in MetaRocq.Common.Reflect]
| 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) |