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 (18986 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 (297 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 (8135 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 (1490 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 (343 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 (524 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 (720 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 (401 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 (331 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 (4701 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 (178 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 (18986 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 (297 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 (8135 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 (1490 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 (343 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 (524 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 (720 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 (401 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 (331 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 (4701 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 (178 entries)