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)

R (abbreviation)

raise [in MetaRocq.SafeChecker.PCUICTypeChecker]
Raw.quote [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote [in MetaRocq.Quotation.ToTemplate.All]
rec [in MetaRocq.SafeChecker.PCUICSafeReduce]
recomp_branch' [in MetaRocq.PCUIC.PCUICReduction]
recomp_branch [in MetaRocq.PCUIC.PCUICReduction]
red_context [in MetaRocq.Erasure.Prelim]
red_terms [in MetaRocq.PCUIC.PCUICConversion]
red_one_branch [in MetaRocq.PCUIC.PCUICReduction]
red_one_context_decl [in MetaRocq.PCUIC.PCUICReduction]
red_one_term [in MetaRocq.PCUIC.PCUICReduction]
red1_ctx_rel [in MetaRocq.PCUIC.PCUICConfluence]
red1_one_branch [in MetaRocq.PCUIC.PCUICReduction]
red1_one_context_decl [in MetaRocq.PCUIC.PCUICReduction]
red1_one_term [in MetaRocq.PCUIC.PCUICReduction]
rename_branch [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branches [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_predicate [in MetaRocq.PCUIC.PCUICSigmaCalculus]
reorder [in MetaRocq.Erasure.EReorderCstrs]
reorder_env [in MetaRocq.Erasure.EReorderCstrs]
reorder_decl [in MetaRocq.Erasure.EReorderCstrs]
repack [in MetaRocq.SafeChecker.PCUICSafeConversion]
ret [in MetaRocq.SafeChecker.PCUICSafeRetyping]
ret [in MetaRocq.SafeChecker.PCUICTypeChecker]
rho_ctx [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_br [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rtrans_clos [in MetaRocq.PCUIC.utils.PCUICOnOne]



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)