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)

U (lemma)

uctx'_eq [in MetaRocq.SafeChecker.PCUICEqualityDec]
udecl_prop_in_var_poly [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
uip_bool [in MetaRocq.Utils.MRUtils]
unfolds_bound [in MetaRocq.Erasure.EWcbvEvalNamed]
unfold_cofix_type [in MetaRocq.Erasure.Prelim]
unfold_length [in MetaRocq.Utils.MRList]
unfold_cofix_wf [in MetaRocq.Template.TypingWf]
unfold_fix_wf [in MetaRocq.Template.TypingWf]
unfold_one_proj_None [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_proj_cored [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_case_None [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_case_cored [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_None [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_decompose [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_cored [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zippx [in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zipp [in MetaRocq.SafeChecker.PCUICSafeConversion]
union_checker_flags_spec [in MetaRocq.Common.config]
unique_sorting_equality_propositional [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_r [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_l [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_r [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_l [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_prop [in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_family [in MetaRocq.PCUIC.PCUICElimination]
unique_type [in MetaRocq.Erasure.ErasureFunctionProperties]
unique_decls [in MetaRocq.Erasure.ErasureFunctionProperties]
UnivConstraint.compare_spec [in MetaRocq.Common.Universes]
UnivConstraint.eq_dec [in MetaRocq.Common.Universes]
UnivConstraint.lt_compat [in MetaRocq.Common.Universes]
UnivConstraint.lt_strorder [in MetaRocq.Common.Universes]
universe_get_is_level_correct [in MetaRocq.Common.Universes]
Universe.make'_inj [in MetaRocq.Common.Universes]
Universe.val_make' [in MetaRocq.Common.Universes]
Universe.val_make [in MetaRocq.Common.Universes]
univ_sup_assoc [in MetaRocq.Common.Universes]
univ_sup_idem [in MetaRocq.Common.Universes]
univ_exprs_map_all [in MetaRocq.PCUIC.PCUICCumulProp]
univ_epxrs_elements_map [in MetaRocq.PCUIC.PCUICCumulProp]
univ_expr_set_in_elements [in MetaRocq.PCUIC.PCUICCumulProp]
untyped_substitution_red [in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_length [in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_nth_error [in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_eq_subst [in MetaRocq.PCUIC.PCUICSpine]
untyped_subslet_skipn [in MetaRocq.PCUIC.PCUICSpine]
untyped_subslet_inds [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_length [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_lift [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_substitution_ws_cumul_pb_subst_conv' [in MetaRocq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb_subst_conv [in MetaRocq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb [in MetaRocq.PCUIC.PCUICConversion]
untyped_closed_red_subst [in MetaRocq.PCUIC.PCUICConversion]
untyped_subslet_def_tip [in MetaRocq.PCUIC.PCUICConversion]
untyped_subslet_extended_subst [in MetaRocq.PCUIC.PCUICContexts]
untyped_subslet_lift [in MetaRocq.PCUIC.PCUICContexts]
untyped_subslet_projs [in MetaRocq.PCUIC.PCUICInductives]
untyped_subslet_inds [in MetaRocq.PCUIC.PCUICCumulProp]
untyped_subslet_ass [in MetaRocq.PCUIC.PCUICConvCumInversion]
ununiquify_level__uniquify_level [in MetaRocq.Common.UniversesDec]
ununiquify_level_level__uniquify_level_level [in MetaRocq.Common.UniversesDec]
ununiquify_level_var__uniquify_level_var [in MetaRocq.Common.UniversesDec]
Upn_subst_consn_lt [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_ge [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_compose [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_Upn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_comp [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_S [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_1 [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_Up [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ren_r [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ren_l [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ren [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_eq [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_1_Up [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_0 [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ctxmap [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Upn_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
upn_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
upto_names_impl_leq_term [in MetaRocq.PCUIC.PCUICEquality]
upto_names_impl_eq_term [in MetaRocq.PCUIC.PCUICEquality]
upto_names_impl [in MetaRocq.PCUIC.PCUICEquality]
upto_eq_impl [in MetaRocq.PCUIC.PCUICEquality]
upto_names_eq_term [in MetaRocq.PCUIC.PCUICAlpha]
upto_names_leq_term [in MetaRocq.PCUIC.PCUICAlpha]
upto_names_eq_term_upto_univ [in MetaRocq.PCUIC.PCUICAlpha]
upto_names_conv_context [in MetaRocq.PCUIC.PCUICAlpha]
upto_names_check_cofix [in MetaRocq.PCUIC.PCUICAlpha]
upto_names_check_fix [in MetaRocq.PCUIC.PCUICAlpha]
upto_names_destInd [in MetaRocq.PCUIC.PCUICAlpha]
Up_comp [in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_ext_closed [in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_up_assoc [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Up_Up_assoc [in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_Upn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_Up [in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_ext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_up [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Up_ctxmap [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
up_ext_cond [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
up_0 [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
Up_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
urename_is_open_term [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urename_on_free_vars_shift [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urenaming_strengthen [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
urenaming_context [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_ext [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vdef [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vass [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_impl [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
UsualIsLeibniz.eq_leibniz [in MetaRocq.Utils.MRMSets]
usubst_well_subst [in MetaRocq.PCUIC.PCUICSubstitution]
usubst_up_vdef [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_up_vass [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_app_up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_app [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_Up' [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_Up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_ext [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_on_free_vars_shift [in MetaRocq.PCUIC.Conversion.PCUICInstConv]


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)