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)

R (instance)

redp_red [in MetaCoq.SafeChecker.PCUICWfReduction]
redp_trans [in MetaCoq.SafeChecker.PCUICWfReduction]
red_brs_refl [in MetaCoq.SafeChecker.PCUICSafeConversion]
red_ctx_alpha_refl [in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_refl [in MetaCoq.PCUIC.PCUICConfluence]
red_Trans [in MetaCoq.PCUIC.PCUICConfluence]
red_Refl [in MetaCoq.PCUIC.PCUICConfluence]
red_terms_refl [in MetaCoq.PCUIC.PCUICConversion]
red_brs_refl [in MetaCoq.PCUIC.PCUICConversion]
ReflectEq_EqDec [in MetaCoq.Template.utils.ReflectEq]
ReflectEq_term [in MetaCoq.Erasure.EReflect]
reflect_eq_projection [in MetaCoq.Template.Kernames]
reflect_eq_inductive [in MetaCoq.Template.Kernames]
reflect_stack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
reflect_choice [in MetaCoq.PCUIC.Syntax.PCUICPosition]
reflect_prod [in MetaCoq.Template.utils.ReflectEq]
reflect_sig_true [in MetaCoq.Template.utils.ReflectEq]
reflect_bool [in MetaCoq.Template.utils.ReflectEq]
reflect_nat [in MetaCoq.Template.utils.ReflectEq]
reflect_list [in MetaCoq.Template.utils.ReflectEq]
reflect_option [in MetaCoq.Template.utils.ReflectEq]
reflect_Variance [in MetaCoq.Template.Reflect]
reflect_allowed_eliminations [in MetaCoq.Template.Reflect]
reflect_universes_decl [in MetaCoq.Template.Reflect]
reflect_ConstraintType [in MetaCoq.Template.Reflect]
reflect_recursivity_kind [in MetaCoq.Template.Reflect]
reflect_case_info [in MetaCoq.Template.Reflect]
reflect_cast_kind [in MetaCoq.Template.Reflect]
reflect_def [in MetaCoq.Template.Reflect]
reflect_aname [in MetaCoq.Template.Reflect]
reflect_relevance [in MetaCoq.Template.Reflect]
reflect_name [in MetaCoq.Template.Reflect]
reflect_levels [in MetaCoq.Template.Reflect]
reflect_prop_level [in MetaCoq.Template.Reflect]
reflect_prim_float [in MetaCoq.Template.Reflect]
reflect_prim_int [in MetaCoq.Template.Reflect]
reflect_term [in MetaCoq.Template.ReflectAst]
reflect_global_decl [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_mutual_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_one_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_projection_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_constructor_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_constant_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_eq_predicate [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_eq_float64 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_eq_spec_float [in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_eq_uint63 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_eq_Z [in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_global_decl [in MetaCoq.Erasure.EReflect]
reflect_mutual_inductive_body [in MetaCoq.Erasure.EReflect]
reflect_one_inductive_body [in MetaCoq.Erasure.EReflect]
reflect_projection_body [in MetaCoq.Erasure.EReflect]
reflect_constructor_body [in MetaCoq.Erasure.EReflect]
reflect_constant_body [in MetaCoq.Erasure.EReflect]
reflexive_equiv [in MetaCoq.Translations.MiniHoTT]
reflexive_paths [in MetaCoq.Translations.MiniHoTT]
reflexive_equiv [in MetaCoq.Translations.MiniHoTT_paths]
reflexive_paths [in MetaCoq.Translations.MiniHoTT_paths]
refl_eq_univ_prop [in MetaCoq.PCUIC.PCUICCumulProp]
relation_disjunction_Symmetric [in MetaCoq.Template.utils.MCRelations]
relation_disjunction_refl_r [in MetaCoq.Template.utils.MCRelations]
relation_disjunction_refl_l [in MetaCoq.Template.utils.MCRelations]
rename_branch_proper [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_predicate_proper [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_proper_pointwise [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_proper [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_telescope_ext [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_context_ext [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
renaming_ext [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ren_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Req_refl [in MetaCoq.SafeChecker.PCUICSafeReduce]
rshiftk_proper [in MetaCoq.PCUIC.PCUICSigmaCalculus]
R_global_instance_impl [in MetaCoq.Template.TermEquality]
R_global_instance_impl_same_napp [in MetaCoq.Template.TermEquality]
R_global_instance_empty_impl [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_impl [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_impl_same_napp [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_antisym [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_equiv [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_equiv [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_trans [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_trans [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_sym [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_refl [in MetaCoq.PCUIC.PCUICEquality]


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)