| 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
labelling_of_valuation [definition, in MetaRocq.Common.uGraph]lam [constructor, in MetaRocq.Examples.add_constructor]
lambdabox_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
lambdabox_pres_fo [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
LambdaNotConvertibleAnn [constructor, in MetaRocq.SafeChecker.PCUICErrors]
LambdaNotConvertibleTypes [constructor, in MetaRocq.SafeChecker.PCUICErrors]
Lambda_bd [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Lambda_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Lambda_conv_cum_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
lam_body_annot_cont [definition, in MetaRocq.Erasure.Typed.Annotations]
lam_tm [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
lam_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
last_nonempty_eq [lemma, in MetaRocq.Utils.MRList]
last_app [lemma, in MetaRocq.Utils.MRList]
last_inv [lemma, in MetaRocq.Utils.MRList]
laxest_checker_flags_laxest [lemma, in MetaRocq.Common.config]
laxest_checker_flags [definition, in MetaRocq.Common.config]
lazy [constructor, in MetaRocq.Template.TemplateMonad.Common]
leb_spect [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
leb_spec_Set [lemma, in MetaRocq.Utils.MRArith]
leb_S [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
left_dlexmod [constructor, in MetaRocq.PCUIC.utils.PCUICUtils]
left_lex [constructor, in MetaRocq.PCUIC.utils.PCUICUtils]
Lemmata [section, in MetaRocq.PCUIC.PCUICSafeLemmata]
Lemmata.cf [variable, in MetaRocq.PCUIC.PCUICSafeLemmata]
Lemmata.flags [variable, in MetaRocq.PCUIC.PCUICSafeLemmata]
Lemmata.hΣ [variable, in MetaRocq.PCUIC.PCUICSafeLemmata]
Lemmata.Σ [variable, in MetaRocq.PCUIC.PCUICSafeLemmata]
len [projection, in MetaRocq.PCUIC.PCUICAst]
len [constructor, in MetaRocq.PCUIC.PCUICAst]
lengths [definition, in MetaRocq.PCUIC.Syntax.PCUICTactics]
lengths [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
length_nil [lemma, in MetaRocq.Utils.MRList]
length_skipn_map [lemma, in MetaRocq.Utils.MRList]
length_skipn [lemma, in MetaRocq.Utils.MRList]
length_rev_map [lemma, in MetaRocq.Utils.MRList]
length_rev [lemma, in MetaRocq.Utils.MRList]
length_rev_transparent [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
length_app_transparent [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
length_skipn_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
length_of [abbreviation, in MetaRocq.PCUIC.PCUICAst]
length_subst_context [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lenm_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
leqb_sort_n_ [definition, in MetaRocq.Common.Universes]
leqb_term_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
leqb_term [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
leqb_term [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
leqb_univ_expr_n_spec' [definition, in MetaRocq.Common.uGraph]
leqb_univ_expr_n_spec_gen' [lemma, in MetaRocq.Common.uGraph]
leqb_sort [definition, in MetaRocq.Common.uGraph]
leqb_universe_n_spec [definition, in MetaRocq.Common.uGraph]
leqb_universe_n_spec_gen [lemma, in MetaRocq.Common.uGraph]
leqb_universe_n_spec0 [definition, in MetaRocq.Common.uGraph]
leqb_universe_n_spec0_gen [lemma, in MetaRocq.Common.uGraph]
leqb_universe_n [definition, in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec [definition, in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec_gen [lemma, in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec0 [definition, in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec0_gen [lemma, in MetaRocq.Common.uGraph]
leqb_expr_univ_n [definition, in MetaRocq.Common.uGraph]
leqb_expr_n_spec [definition, in MetaRocq.Common.uGraph]
leqb_expr_n_spec_gen [lemma, in MetaRocq.Common.uGraph]
leqb_expr_n_spec0 [definition, in MetaRocq.Common.uGraph]
leqb_expr_n_spec0_gen [lemma, in MetaRocq.Common.uGraph]
leqb_expr_n [definition, in MetaRocq.Common.uGraph]
leqb_level_n_spec [lemma, in MetaRocq.Common.uGraph]
leqb_level_n_spec_gen [definition, in MetaRocq.Common.uGraph]
leqb_level_n [definition, in MetaRocq.Common.uGraph]
leqb_sort_gen [definition, in MetaRocq.Common.uGraph]
leqb_universe_n_gen [definition, in MetaRocq.Common.uGraph]
leqb_expr_univ_n_gen [definition, in MetaRocq.Common.uGraph]
leqb_expr_n_gen [definition, in MetaRocq.Common.uGraph]
leq_term_mkApps [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
leq_term_App [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
leq_term_leq_term_napp [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
leq_term_leq_term_napp [lemma, in MetaRocq.PCUIC.PCUICEquality]
leq_term_partial_order [instance, in MetaRocq.PCUIC.PCUICEquality]
leq_term_antisym [instance, in MetaRocq.PCUIC.PCUICEquality]
leq_term_preorder [instance, in MetaRocq.PCUIC.PCUICEquality]
leq_context_preord [instance, in MetaRocq.PCUIC.PCUICEquality]
leq_context [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
leq_decl [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
leq_term [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
leq_term_prop_sorted_r [lemma, in MetaRocq.PCUIC.PCUICElimination]
leq_term_prop_sorted_l [lemma, in MetaRocq.PCUIC.PCUICElimination]
leq_sort_propositional_l [lemma, in MetaRocq.PCUIC.PCUICElimination]
leq_prop_is_propositonal [lemma, in MetaRocq.Common.Universes]
leq_sort_prop_no_prop_sub_type [lemma, in MetaRocq.Common.Universes]
leq_sort_super [lemma, in MetaRocq.Common.Universes]
leq_sort_product_mon [lemma, in MetaRocq.Common.Universes]
leq_sort_config_impl [lemma, in MetaRocq.Common.Universes]
leq_universe_config_impl [lemma, in MetaRocq.Common.Universes]
leq_sort_subset [lemma, in MetaRocq.Common.Universes]
leq_sort_refl' [definition, in MetaRocq.Common.Universes]
leq_sort_product [lemma, in MetaRocq.Common.Universes]
leq_sort_sup_r [lemma, in MetaRocq.Common.Universes]
leq_sort_sup_l [lemma, in MetaRocq.Common.Universes]
leq_csort_of_product_mon [lemma, in MetaRocq.Common.Universes]
leq_csort [definition, in MetaRocq.Common.Universes]
leq_csort_n [definition, in MetaRocq.Common.Universes]
leq_sort_partial_order [instance, in MetaRocq.Common.Universes]
leq_sort_antisym [instance, in MetaRocq.Common.Universes]
leq_sort_preorder [instance, in MetaRocq.Common.Universes]
leq_sort_trans [instance, in MetaRocq.Common.Universes]
leq_sort_n_trans [instance, in MetaRocq.Common.Universes]
leq_sort_refl [instance, in MetaRocq.Common.Universes]
leq_sort_leq_sort_n [lemma, in MetaRocq.Common.Universes]
leq_sort [definition, in MetaRocq.Common.Universes]
leq_sort_n [definition, in MetaRocq.Common.Universes]
leq_sort_n_ [definition, in MetaRocq.Common.Universes]
leq_universe_subset [lemma, in MetaRocq.Common.Universes]
leq_universe_refl' [definition, in MetaRocq.Common.Universes]
leq_universe_partial_order [instance, in MetaRocq.Common.Universes]
leq_universe_antisym [instance, in MetaRocq.Common.Universes]
leq_universe_preorder [instance, in MetaRocq.Common.Universes]
leq_universe_sup_mon [lemma, in MetaRocq.Common.Universes]
leq_universe_sup_r [lemma, in MetaRocq.Common.Universes]
leq_universe_sup_l [lemma, in MetaRocq.Common.Universes]
leq_universe_trans [instance, in MetaRocq.Common.Universes]
leq_universe_n_trans [instance, in MetaRocq.Common.Universes]
leq_universe_refl [instance, in MetaRocq.Common.Universes]
leq_universe [definition, in MetaRocq.Common.Universes]
leq_universe_n [definition, in MetaRocq.Common.Universes]
leq_sort_sort_of_products [lemma, in MetaRocq.PCUIC.PCUICSpine]
leq_term_subset [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
leq_term_App [lemma, in MetaRocq.Template.TermEquality]
leq_term_mkApps [lemma, in MetaRocq.Template.TermEquality]
leq_term_refl [lemma, in MetaRocq.Template.TermEquality]
leq_term [abbreviation, in MetaRocq.Template.TermEquality]
leq_sortP_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
leq_universeP_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
leq_universe_n_dec [definition, in MetaRocq.Common.UniversesDec]
leq_term_propositional_sorted_l [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
leq_sort_sort_of_products_mon [lemma, in MetaRocq.PCUIC.PCUICArities]
leq_term_nocast [definition, in MetaRocq.Template.Typing]
leq_term [definition, in MetaRocq.Template.Checker]
leq_term_napp [abbreviation, in MetaRocq.PCUIC.PCUICCumulProp]
leq_term_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_sort_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_universe_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_universe_SubstUnivPreserving [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_sort_propositional_l [lemma, in MetaRocq.Erasure.EArities]
leq_sort_propositional_r [lemma, in MetaRocq.Erasure.EArities]
leq_term_propopositional_sorted_r [lemma, in MetaRocq.Erasure.EArities]
leq_term_propositional_sorted_l [lemma, in MetaRocq.Erasure.EArities]
leq_term_config_impl [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
leq_universe_vertices [lemma, in MetaRocq.Common.uGraph]
leq_universe_vertices1 [lemma, in MetaRocq.Common.uGraph]
leq_universe_vertices0 [lemma, in MetaRocq.Common.uGraph]
leq_term_empty_leq_term [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
leq0_universe_n [definition, in MetaRocq.Common.Universes]
leq0_universe_n_dec [definition, in MetaRocq.Common.UniversesDec]
leq0_level_n_complete [definition, in MetaRocq.Common.uGraph]
leq0_level_n_complete_gen [lemma, in MetaRocq.Common.uGraph]
leq0_level_n [definition, in MetaRocq.Common.uGraph]
LetIn_in [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
LetIn_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
LetIn_bd [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
letin_red_body [constructor, in MetaRocq.Template.Typing]
letin_red_ty [constructor, in MetaRocq.Template.Typing]
letin_red_def [constructor, in MetaRocq.Template.Typing]
letin_red_body [constructor, in MetaRocq.PCUIC.PCUICReduction]
letin_red_ty [constructor, in MetaRocq.PCUIC.PCUICReduction]
letin_red_def [constructor, in MetaRocq.PCUIC.PCUICReduction]
lets_in_constructor_types [projection, in MetaRocq.Common.config]
let_in [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
let_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
let_bd [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Level [module, in MetaRocq.Common.Universes]
LevelExpr [module, in MetaRocq.Common.Universes]
LevelExprSet [module, in MetaRocq.Common.Universes]
LevelExprSetDecide [module, in MetaRocq.Common.Universes]
LevelExprSetExtraOrdProp [module, in MetaRocq.Common.Universes]
LevelExprSetFact [module, in MetaRocq.Common.Universes]
LevelExprSetOrdProp [module, in MetaRocq.Common.Universes]
LevelExprSetProp [module, in MetaRocq.Common.Universes]
levelexprset_eq_dec [instance, in MetaRocq.Common.Universes]
levelexprset_reflect [instance, in MetaRocq.Common.Universes]
LevelExprSet_For_all [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
LevelExpr.compare [definition, in MetaRocq.Common.Universes]
LevelExpr.compare_spec [definition, in MetaRocq.Common.Universes]
LevelExpr.eq [definition, in MetaRocq.Common.Universes]
LevelExpr.eq_leibniz [definition, in MetaRocq.Common.Universes]
LevelExpr.eq_dec [definition, in MetaRocq.Common.Universes]
LevelExpr.eq_equiv [definition, in MetaRocq.Common.Universes]
LevelExpr.Evaluable [instance, in MetaRocq.Common.Universes]
LevelExpr.get_noprop [definition, in MetaRocq.Common.Universes]
LevelExpr.get_level [definition, in MetaRocq.Common.Universes]
LevelExpr.is_level [definition, in MetaRocq.Common.Universes]
LevelExpr.lt [definition, in MetaRocq.Common.Universes]
LevelExpr.ltLevelExpr1 [constructor, in MetaRocq.Common.Universes]
LevelExpr.ltLevelExpr2 [constructor, in MetaRocq.Common.Universes]
LevelExpr.lt_compat [definition, in MetaRocq.Common.Universes]
LevelExpr.lt_strorder [instance, in MetaRocq.Common.Universes]
LevelExpr.lt__sind [definition, in MetaRocq.Common.Universes]
LevelExpr.lt__ind [definition, in MetaRocq.Common.Universes]
LevelExpr.lt_ [inductive, in MetaRocq.Common.Universes]
LevelExpr.make [definition, in MetaRocq.Common.Universes]
LevelExpr.reflect_t [instance, in MetaRocq.Common.Universes]
LevelExpr.set [definition, in MetaRocq.Common.Universes]
LevelExpr.succ [definition, in MetaRocq.Common.Universes]
LevelExpr.t [definition, in MetaRocq.Common.Universes]
LevelExpr.type1 [definition, in MetaRocq.Common.Universes]
LevelExpr.val_make_npl [lemma, in MetaRocq.Common.Universes]
LevelExpr.val_make [lemma, in MetaRocq.Common.Universes]
LevelIn_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
LevelSet [module, in MetaRocq.Common.Universes]
LevelSetDecide [module, in MetaRocq.Common.Universes]
LevelSetExtraDecide [module, in MetaRocq.Common.Universes]
LevelSetExtraOrdProp [module, in MetaRocq.Common.Universes]
LevelSetFact [module, in MetaRocq.Common.Universes]
LevelSetMoreFacts [section, in MetaRocq.Common.Universes]
LevelSetOrdProp [module, in MetaRocq.Common.Universes]
LevelSetProp [module, in MetaRocq.Common.Universes]
LevelSetsUIP [module, in MetaRocq.Common.Reflect]
LevelSetsUIP.eqb_LevelSet [definition, in MetaRocq.Common.Reflect]
LevelSetsUIP.levels_tree_reflect [instance, in MetaRocq.Common.Reflect]
LevelSetsUIP.levels_tree_rect [definition, in MetaRocq.Common.Reflect]
LevelSetsUIP.levels_tree_eqb [definition, in MetaRocq.Common.Reflect]
LevelSetsUIP.ok_irrel [lemma, in MetaRocq.Common.Reflect]
LevelSetsUIP.reflect_LevelSet [instance, in MetaRocq.Common.Reflect]
LevelSet_union_empty [lemma, in MetaRocq.Common.Universes]
LevelSet_In_fold_right_add [lemma, in MetaRocq.Common.Universes]
LevelSet_mem_union [definition, in MetaRocq.Common.Universes]
LevelSet_pair_In [lemma, in MetaRocq.Common.Universes]
LevelSet_pair [definition, in MetaRocq.Common.Universes]
LevelSet_In_declare_and_uniquify_and_combine_levels_1_1 [lemma, in MetaRocq.Common.UniversesDec]
LevelSet_In_fold_add [lemma, in MetaRocq.Common.UniversesDec]
LevelSet_in_union_global [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
levelset_for_all_eq [lemma, in MetaRocq.Common.uGraph]
levels_of_udecl [definition, in MetaRocq.Common.Universes]
levels_of_universe_spec [lemma, in MetaRocq.Common.UniversesDec]
levels_of_universe [definition, in MetaRocq.Common.UniversesDec]
levels_of_cscs_spec [lemma, in MetaRocq.Common.UniversesDec]
levels_of_cscs [definition, in MetaRocq.Common.UniversesDec]
levels_of_cs2_spec [lemma, in MetaRocq.Common.UniversesDec]
levels_of_cs2 [definition, in MetaRocq.Common.UniversesDec]
levels_of_cs_spec [lemma, in MetaRocq.Common.UniversesDec]
levels_of_cs [definition, in MetaRocq.Common.UniversesDec]
levels_global_levels_declared [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
levels_global_ext_constraint [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_global_constraint [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_univ_gc_declared_declared [lemma, in MetaRocq.Common.uGraph]
levels_gc_declared_declared [lemma, in MetaRocq.Common.uGraph]
level_lt_ind_dep [definition, in MetaRocq.Common.Reflect]
level_var_instance_length [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
level_mem [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
level_gc_declared_declared [lemma, in MetaRocq.Common.uGraph]
Level.compare [definition, in MetaRocq.Common.Universes]
Level.compare_spec [definition, in MetaRocq.Common.Universes]
Level.eq [definition, in MetaRocq.Common.Universes]
Level.eqb [definition, in MetaRocq.Common.Universes]
Level.eqb_spec [lemma, in MetaRocq.Common.Universes]
Level.eqb_refl [instance, in MetaRocq.Common.Universes]
Level.eq_dec [definition, in MetaRocq.Common.Universes]
Level.eq_leibniz [definition, in MetaRocq.Common.Universes]
Level.eq_level [definition, in MetaRocq.Common.Universes]
Level.eq_equiv [definition, in MetaRocq.Common.Universes]
Level.Evaluable [instance, in MetaRocq.Common.Universes]
Level.is_var [definition, in MetaRocq.Common.Universes]
Level.is_set [definition, in MetaRocq.Common.Universes]
Level.level [constructor, in MetaRocq.Common.Universes]
Level.lt [definition, in MetaRocq.Common.Universes]
Level.ltLevelLevel [constructor, in MetaRocq.Common.Universes]
Level.ltLevellvar [constructor, in MetaRocq.Common.Universes]
Level.ltlvarlvar [constructor, in MetaRocq.Common.Universes]
Level.ltSetLevel [constructor, in MetaRocq.Common.Universes]
Level.ltSetlvar [constructor, in MetaRocq.Common.Universes]
Level.lt_compat [definition, in MetaRocq.Common.Universes]
Level.lt_strorder [definition, in MetaRocq.Common.Universes]
Level.lt__sind [definition, in MetaRocq.Common.Universes]
Level.lt__ind [definition, in MetaRocq.Common.Universes]
Level.lt_ [inductive, in MetaRocq.Common.Universes]
Level.lvar [constructor, in MetaRocq.Common.Universes]
Level.lzero [constructor, in MetaRocq.Common.Universes]
Level.reflect_level [instance, in MetaRocq.Common.Universes]
Level.t [definition, in MetaRocq.Common.Universes]
Level.t__sind [definition, in MetaRocq.Common.Universes]
Level.t__rec [definition, in MetaRocq.Common.Universes]
Level.t__ind [definition, in MetaRocq.Common.Universes]
Level.t__rect [definition, in MetaRocq.Common.Universes]
Level.t_ [inductive, in MetaRocq.Common.Universes]
lexprod [definition, in MetaRocq.PCUIC.utils.PCUICUtils]
le_ind_prop [definition, in MetaRocq.Common.Reflect]
le_irrel [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
liat [abbreviation, in MetaRocq.PCUIC.PCUICValidity]
Lib [library]
LibHypsNaming [library]
lift [definition, in MetaRocq.PCUIC.PCUICAst]
lift [definition, in MetaRocq.Template.Ast]
lift [definition, in MetaRocq.Erasure.ELiftSubst]
liftP_ctx [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
liftP_ctx_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
LiftSubst [library]
lift_unlift_context [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift_term [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
lift_judgment_SR [lemma, in MetaRocq.PCUIC.PCUICSR]
lift_leq_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
lift_eq_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
lift_compare_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
lift_compare_decls [lemma, in MetaRocq.PCUIC.PCUICEquality]
lift_compare_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
lift_extended_subst' [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_extended_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_alt [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc0 [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_decl0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_to_extended_list_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_closed [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_isApp [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_lt [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_ge [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_declared_constant [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
lift_context_add [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
lift_decl_closed [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
lift_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICSpine]
lift_context0_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
lift_context_subst_context [lemma, in MetaRocq.PCUIC.PCUICSpine]
lift_namesM [definition, in MetaRocq.Template.AstUtils]
lift_names [definition, in MetaRocq.Template.AstUtils]
lift_typing_wf_local [lemma, in MetaRocq.PCUIC.PCUICTyping]
lift_to_pred [lemma, in MetaRocq.PCUIC.PCUICConfluence]
lift_to_ws_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
lift_ws [definition, in MetaRocq.PCUIC.PCUICConfluence]
lift_ctx [definition, in MetaRocq.Template.EtaExpand]
lift_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
lift_wt_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
lift_sorting_lift_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
lift_to_extended_list_k [lemma, in MetaRocq.Template.LiftSubst]
lift_closed [lemma, in MetaRocq.Template.LiftSubst]
lift_mkApps [lemma, in MetaRocq.Template.LiftSubst]
lift_rel_lt [lemma, in MetaRocq.Template.LiftSubst]
lift_rel_ge [lemma, in MetaRocq.Template.LiftSubst]
lift_instance_length [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
lift_isApp [lemma, in MetaRocq.Template.WfAst]
lift_to_wf_list [lemma, in MetaRocq.Template.WfAst]
lift_to_list [lemma, in MetaRocq.Template.WfAst]
lift_judgment_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
lift_wfext [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
lift_renaming_0 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_rename [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_renaming_0_rshift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_renaming_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_renaming [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_isLambda [lemma, in MetaRocq.Erasure.ESubstitution]
lift_inst_case_branch_context [lemma, in MetaRocq.Erasure.ESubstitution]
lift_iota_red [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
lift_rename' [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
lift_context_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
lift_context_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICInductives]
lift_context_subst_context_let_expand [lemma, in MetaRocq.PCUIC.PCUICInductives]
lift_context_lift_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
lift_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_fix_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_mutual_inductive_body [definition, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_context_lift_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_typing2_wf_pred [lemma, in MetaRocq.Template.TypingWf]
lift_typing_wf_pred [lemma, in MetaRocq.Template.TypingWf]
lift_context_snoc [lemma, in MetaRocq.Template.TypingWf]
lift_context_snoc0 [definition, in MetaRocq.Template.TypingWf]
lift_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lift_dearg_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lift_dearg_single [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lift_wt_inv [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
lift_typing_is_open_term [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
lift_closed [lemma, in MetaRocq.Erasure.ELiftSubst]
lift_mkApps [lemma, in MetaRocq.Erasure.ELiftSubst]
lift_isApp [lemma, in MetaRocq.Erasure.ELiftSubst]
lift_rel_alt [lemma, in MetaRocq.Erasure.ELiftSubst]
lift_rel_lt [lemma, in MetaRocq.Erasure.ELiftSubst]
lift_rel_ge [lemma, in MetaRocq.Erasure.ELiftSubst]
lift0 [abbreviation, in MetaRocq.PCUIC.PCUICAst]
lift0 [abbreviation, in MetaRocq.Template.Ast]
lift0 [abbreviation, in MetaRocq.Erasure.ELiftSubst]
lift0_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift0_p [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift0_id [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift0_open [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
lift0_p [lemma, in MetaRocq.Template.LiftSubst]
lift0_id [lemma, in MetaRocq.Template.LiftSubst]
lift0_rename [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift0_inst_id [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
lift0_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
lift0_p [lemma, in MetaRocq.Erasure.ELiftSubst]
lift0_id [lemma, in MetaRocq.Erasure.ELiftSubst]
Listable [record, in MetaRocq.Utils.MRListable]
ListOrderedType [module, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_trans [lemma, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_lt_lt [lemma, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_sym [lemma, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_refl [lemma, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_eq [lemma, in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_spec [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.eq [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.eqb [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.eqb_dec [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.eq_dec [instance, in MetaRocq.Utils.MRCompare]
ListOrderedType.eq_leibniz [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.eq_equiv [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt_compat [instance, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt_strorder [instance, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt__sind [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt__ind [definition, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt_cons_cons_tl [constructor, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt_cons_cons_hd [constructor, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt_nil_cons [constructor, in MetaRocq.Utils.MRCompare]
ListOrderedType.lt_ [inductive, in MetaRocq.Utils.MRCompare]
ListOrderedType.t [definition, in MetaRocq.Utils.MRCompare]
ListSize [section, in MetaRocq.Utils.MRList]
ListSizeMap [section, in MetaRocq.Utils.MRList]
ListSizeMap.A [variable, in MetaRocq.Utils.MRList]
ListSizeMap.B [variable, in MetaRocq.Utils.MRList]
ListSizeMap.sizeA [variable, in MetaRocq.Utils.MRList]
ListSizeMap.sizeB [variable, in MetaRocq.Utils.MRList]
ListSize.A [variable, in MetaRocq.Utils.MRList]
ListSize.size [variable, in MetaRocq.Utils.MRList]
list_size_length [lemma, in MetaRocq.Examples.tauto]
list_size_map_hom [lemma, in MetaRocq.Utils.MRList]
list_size_map_le [lemma, in MetaRocq.Utils.MRList]
list_size_mapi_le [lemma, in MetaRocq.Utils.MRList]
list_size_mapi_rec_le [lemma, in MetaRocq.Utils.MRList]
list_size_map_eq [lemma, in MetaRocq.Utils.MRList]
list_size_mapi_eq [lemma, in MetaRocq.Utils.MRList]
list_size_mapi_rec_eq [lemma, in MetaRocq.Utils.MRList]
list_size_map [lemma, in MetaRocq.Utils.MRList]
list_size_length [lemma, in MetaRocq.Utils.MRList]
list_size_rev [lemma, in MetaRocq.Utils.MRList]
list_size_app [lemma, in MetaRocq.Utils.MRList]
list_size [definition, in MetaRocq.Utils.MRList]
list_rect_rev [lemma, in MetaRocq.Utils.MRList]
list_ind_rev [lemma, in MetaRocq.Utils.MRList]
list_all [projection, in MetaRocq.Utils.MRListable]
list_size_skipn [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
list_length_ind [lemma, in MetaRocq.Template.LiftSubst]
list_length_rev_ind [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
list_size_rev [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
list_size_mapi_context_hom [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
list_depth_mapi_rec_le [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_depth_rev [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_depth_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_depth [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_map_swap_eq' [lemma, in MetaRocq.PCUIC.PCUICReduction]
list_map_swap_eq [lemma, in MetaRocq.PCUIC.PCUICReduction]
list_split_eq [lemma, in MetaRocq.PCUIC.PCUICReduction]
list_context_sind [definition, in MetaRocq.PCUIC.PCUICReduction]
list_context_rec [definition, in MetaRocq.PCUIC.PCUICReduction]
list_context_ind [definition, in MetaRocq.PCUIC.PCUICReduction]
list_context_rect [definition, in MetaRocq.PCUIC.PCUICReduction]
list_context [inductive, in MetaRocq.PCUIC.PCUICReduction]
Loader [library]
Loader [library]
Loader [library]
Loader [library]
local [constructor, in MetaRocq.Template.TemplateMonad.Common]
LocalAssum [constructor, in MetaRocq.PCUIC.PCUICAst]
LocalAssum [constructor, in MetaRocq.Erasure.EAst]
localassum_cons_def [constructor, in MetaRocq.PCUIC.PCUICElimination]
localassum_cons_abs [constructor, in MetaRocq.PCUIC.PCUICElimination]
localassum_nil [constructor, in MetaRocq.PCUIC.PCUICElimination]
LocalDef [constructor, in MetaRocq.PCUIC.PCUICAst]
LocalDef [constructor, in MetaRocq.Erasure.EAst]
locality [inductive, in MetaRocq.Template.TemplateMonad.Common]
local_env_telescope [lemma, in MetaRocq.PCUIC.PCUICConfluence]
local_entry_sind [definition, in MetaRocq.PCUIC.PCUICAst]
local_entry_rec [definition, in MetaRocq.PCUIC.PCUICAst]
local_entry_ind [definition, in MetaRocq.PCUIC.PCUICAst]
local_entry_rect [definition, in MetaRocq.PCUIC.PCUICAst]
local_entry [inductive, in MetaRocq.PCUIC.PCUICAst]
local_entry_sind [definition, in MetaRocq.Erasure.EAst]
local_entry_rec [definition, in MetaRocq.Erasure.EAst]
local_entry_ind [definition, in MetaRocq.Erasure.EAst]
local_entry_rect [definition, in MetaRocq.Erasure.EAst]
local_entry [inductive, in MetaRocq.Erasure.EAst]
local_env_telescope [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Lookup [module, in MetaRocq.Common.EnvironmentTyping]
lookup [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
lookup [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
lookups [section, in MetaRocq.PCUIC.utils.PCUICPretty]
Lookups [section, in MetaRocq.Template.Checker]
Lookups [section, in MetaRocq.Erasure.EGlobalEnv]
LookupSig [module, in MetaRocq.Common.EnvironmentTyping]
lookups.Σ [variable, in MetaRocq.PCUIC.utils.PCUICPretty]
Lookups.Σ [variable, in MetaRocq.Template.Checker]
Lookups.Σ [variable, in MetaRocq.Erasure.EGlobalEnv]
lookup_env_nlg [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
lookup_constructor_pars_args_implement_box [lemma, in MetaRocq.Erasure.EImplementBox]
lookup_inductive_implement_box [lemma, in MetaRocq.Erasure.EImplementBox]
lookup_constructor_implement_box [lemma, in MetaRocq.Erasure.EImplementBox]
lookup_env_implement_box [lemma, in MetaRocq.Erasure.EImplementBox]
lookup_constructor_pars_args_spec [lemma, in MetaRocq.Erasure.EImplementBox]
lookup_ind_decl [definition, in MetaRocq.Template.Pretty]
lookup_global_deps [lemma, in MetaRocq.Erasure.ErasureFunction]
lookup_env_In [lemma, in MetaRocq.Erasure.ErasureFunction]
lookup_constructor_full [definition, in MetaRocq.Erasure.Typed.ExAst]
lookup_constructor [definition, in MetaRocq.Erasure.Typed.ExAst]
lookup_inductive [definition, in MetaRocq.Erasure.Typed.ExAst]
lookup_minductive [definition, in MetaRocq.Erasure.Typed.ExAst]
lookup_constant [definition, in MetaRocq.Erasure.Typed.ExAst]
lookup_env [definition, in MetaRocq.Erasure.Typed.ExAst]
lookup_env_Some_fresh [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
lookup_global_Some_fresh [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
lookup_inductive [definition, in MetaRocq.Template.AstUtils]
lookup_minductive [definition, in MetaRocq.Template.AstUtils]
lookup_mind_decl [definition, in MetaRocq.Template.AstUtils]
lookup_projection_lookup_constructor [lemma, in MetaRocq.Erasure.ErasureProperties]
lookup_constant [definition, in MetaRocq.Erasure.ErasureProperties]
lookup_inductive_pars_unbox [lemma, in MetaRocq.Erasure.EUnboxing]
lookup_constructor_pars_args_unbox [lemma, in MetaRocq.Erasure.EUnboxing]
lookup_constructor_unbox [lemma, in MetaRocq.Erasure.EUnboxing]
lookup_env_unbox [lemma, in MetaRocq.Erasure.EUnboxing]
lookup_ind_decl_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
lookup_ind_decl [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
lookup_env_cons_fresh [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
lookup_env_cons [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
lookup_env_nil [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
lookup_erase_global [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_global_app_wf [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_erase_decl [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_In_map_fst [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_erase_global_diff [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_erase_decl_None [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_cons_disc [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_env_ext [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
lookup_global_extends [lemma, in MetaRocq.Template.EtaExpand]
lookup_env_Some_fresh [lemma, in MetaRocq.Template.EtaExpand]
lookup_global_Some_fresh [lemma, in MetaRocq.Template.EtaExpand]
lookup_global_map_on_snd [lemma, in MetaRocq.Template.EtaExpand]
lookup_lookup_global_env_None [lemma, in MetaRocq.Template.EtaExpand]
lookup_global_env_lookup [lemma, in MetaRocq.Template.EtaExpand]
lookup_lookup_global_env [lemma, in MetaRocq.Template.EtaExpand]
lookup_global_env [definition, in MetaRocq.Template.EtaExpand]
lookup_env_find [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
lookup_globals_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
lookup_projection_gen_transform [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
lookup_constructor_gen_transform [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_gen_transform [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_gen_transform_env_None [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_map_snd [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_gen_transform_env_Some [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
lookup_env_In [lemma, in MetaRocq.Erasure.EExtends]
lookup_ind_decl [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
lookup_constructor_pars_args_nopars [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
lookup_constructor_pars_args_lookup_inductive_pars [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
lookup_env_in_erase_global_deps [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
lookup_inductive_pars_constructor_pars_args [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
lookup_global_In_wf [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
lookup_env_In [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
lookup_constructor_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_inductive_pars_optimize [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_remove_match_on_box_env_None [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_map_snd [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_env_remove_match_on_box_env_Some [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
lookup_projection_gen_transform [lemma, in MetaRocq.Erasure.EGenericMapEnv]
lookup_constructor_gen_transform [lemma, in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_gen_transform [lemma, in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_None [lemma, in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_map_snd [lemma, in MetaRocq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_Some [lemma, in MetaRocq.Erasure.EGenericMapEnv]
lookup_inductive_pars_optimize [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_projection_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_projection_ordinal [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc_None_reorder_one_ind [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc_wf_tags [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc_spec [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_constant_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_env_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_ordinal [definition, in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_mapping [definition, in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc [definition, in MetaRocq.Erasure.EReorderCstrs]
lookup_declared_constructor [lemma, in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_transform_blocks [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_inductive_transform_blocks [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_env_transform_blocks [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_constructor_pars_args_spec [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
lookup_env_In_map_fst [lemma, in MetaRocq.ErasurePlugin.ETransform]
lookup_env_closed [lemma, in MetaRocq.Erasure.EWcbvEval]
lookup_inductive_map_on_snd_remove_decl [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_inductive_erase_global_decls_deps [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_lookup_global_env_None [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_inductive_filter_deps_None [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_inductive_filter_deps_Some [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_env_filter_deps_None [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_env_filter_deps [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_env_filter [lemma, in MetaRocq.ErasurePlugin.Erasure]
lookup_env [definition, in MetaRocq.Template.Checker]
lookup_constructor_type_cstrs [definition, in MetaRocq.Template.Checker]
lookup_constructor_type [definition, in MetaRocq.Template.Checker]
lookup_constructor_decl [definition, in MetaRocq.Template.Checker]
lookup_ind_type_cstrs [definition, in MetaRocq.Template.Checker]
lookup_ind_type [definition, in MetaRocq.Template.Checker]
lookup_ind_decl [definition, in MetaRocq.Template.Checker]
lookup_constant_type_cstrs [definition, in MetaRocq.Template.Checker]
lookup_constant_type [definition, in MetaRocq.Template.Checker]
lookup_in_env [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
lookup_annotate_env [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
lookup_ind_decl [definition, in MetaRocq.Erasure.EPretty]
lookup_env_wellformed [lemma, in MetaRocq.Erasure.EWellformed]
lookup_env_extends [lemma, in MetaRocq.Template.TypingWf]
lookup_projection_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_constructor_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_inductive_pars_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_env_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_env_optimize_env_None [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_env_map_snd [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_env_optimize_env_Some [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_inductive_wellformed [lemma, in MetaRocq.Erasure.EInlineProjections]
lookup_constructor_debox_types [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_debox_env_types [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_lookup_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_trans_env_inv [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_ctor_trans_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_dearg_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_Forall [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_env_trans_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
lookup_inductive_declared [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
lookup_ind_decl [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
lookup_env_Some_fresh [lemma, in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor_pars_args_cstr_arity [lemma, in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor_lookup_inductive [lemma, in MetaRocq.Erasure.EGlobalEnv]
lookup_projection_lookup_constructor [lemma, in MetaRocq.Erasure.EGlobalEnv]
lookup_projection [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor_pars_args [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_inductive_kind [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_inductive_pars [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_inductive [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_minductive [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_constant [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_env [definition, in MetaRocq.Erasure.EGlobalEnv]
lookup_minductive_declared_inductive [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_minductive_declared_minductive [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_spec [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_constructor_lookup_inductive_pars [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_is_prop_and_pars [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_constructor_pars_args_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_constructor_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_env_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_pars_constructor_pars_args [lemma, in MetaRocq.Erasure.ERemoveParams]
lookup_inductive_None [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
lookup_lookup_env [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
lookup_constructor_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_trans_env_None [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_map_snd [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
lookup_env_trans_env_Some [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
Lookup.consistent_instance_length [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.consistent_instance_ext [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.consistent_instance [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_ind_declared_constructors [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_projection_lookup_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constructor_lookup_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_inductive_lookup_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_minductive_lookup_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constant_lookup_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_projection [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_projection_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constructor [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constructor_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_inductive [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_inductive_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_minductive [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_minductive_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constant [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constant_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_levels_InSet [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_uctx [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_constraints [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_levels [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_uctx [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_constraints [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_levels_memSet [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_levels_InSet [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.global_levels [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_projection_declared_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constructor_declared_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_inductive_declared_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_minductive_declared_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constant_declared_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_projection [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_projection_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constructor [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constructor_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_inductive [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_inductive_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_minductive [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_minductive_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constant [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constant_gen [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.on_udecl_decl [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.universes_decl_of_decl [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_sort_dec [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_universe_dec [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_sort [definition, in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_universe [definition, in MetaRocq.Common.EnvironmentTyping]
LS [module, in MetaRocq.Common.Universes]
LSet_in_global_bounded [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
LSet_in_poly_bounded [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
lsp_proper [instance, in MetaRocq.Common.uGraph]
lsp_expr [definition, in MetaRocq.Common.uGraph]
lt [definition, in MetaRocq.Utils.ByteCompareSpec]
lt_not_eq [lemma, in MetaRocq.Utils.ByteCompareSpec]
lt_trans [lemma, in MetaRocq.Utils.ByteCompareSpec]
lt_sort_str_order' [instance, in MetaRocq.Common.Universes]
lt_sort_irrefl' [instance, in MetaRocq.Common.Universes]
lt_csort [definition, in MetaRocq.Common.Universes]
lt_sort_str_order [instance, in MetaRocq.Common.Universes]
lt_sort_irrefl [lemma, in MetaRocq.Common.Universes]
lt_sort_trans [instance, in MetaRocq.Common.Universes]
lt_sort [definition, in MetaRocq.Common.Universes]
lt_universe_str_order [instance, in MetaRocq.Common.Universes]
lt_universe_irrefl [instance, in MetaRocq.Common.Universes]
lt_universe_trans [instance, in MetaRocq.Common.Universes]
lt_universe [definition, in MetaRocq.Common.Universes]
lt_level_irrel [lemma, in MetaRocq.Common.Reflect]
lzero [abbreviation, in MetaRocq.Common.uGraph]
| 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) |