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 (definition)

R [in MetaCoq.SafeChecker.PCUICSafeReduce]
R [in MetaCoq.SafeChecker.PCUICSafeConversion]
rebuild_case_branch_ctx [in MetaCoq.Template.Checker]
rebuild_case_predicate_ctx [in MetaCoq.Template.Checker]
rebuild_wf_env_transform [in MetaCoq.Erasure.ETransform]
rebuild_wf_env [in MetaCoq.Erasure.ETransform]
red [in MetaCoq.PCUIC.PCUICReduction]
RedFlags.default [in MetaCoq.PCUIC.PCUICNormal]
RedFlags.default [in MetaCoq.Template.Checker]
RedFlags.nodelta [in MetaCoq.PCUIC.PCUICNormal]
redl_branch [in MetaCoq.PCUIC.PCUICReduction]
redl_context [in MetaCoq.PCUIC.PCUICReduction]
redl_term [in MetaCoq.PCUIC.PCUICReduction]
redp [in MetaCoq.SafeChecker.PCUICWfReduction]
redp_subterm_rel [in MetaCoq.SafeChecker.PCUICWfReduction]
reduce [in MetaCoq.Template.Checker]
reduce_stack_eq [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_stack_eq [in MetaCoq.Erasure.ErasureFunction]
reduce_to_ind [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_prod [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_sort [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_term [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_full [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_ind [in MetaCoq.Template.Checker]
reduce_to_prod [in MetaCoq.Template.Checker]
reduce_to_sort [in MetaCoq.Template.Checker]
reduce_opt [in MetaCoq.Template.Checker]
reduce_stack_term [in MetaCoq.Template.Checker]
reduce_stack [in MetaCoq.Template.Checker]
reducible_head [in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head [in MetaCoq.Template.Checker]
red_viewc [in MetaCoq.SafeChecker.PCUICSafeReduce]
red_discr [in MetaCoq.SafeChecker.PCUICSafeReduce]
red_ctx_alpha [in MetaCoq.PCUIC.PCUICConfluence]
red_rel_ctx [in MetaCoq.PCUIC.PCUICConfluence]
red_ctx [in MetaCoq.PCUIC.PCUICConfluence]
red_brs [in MetaCoq.PCUIC.PCUICReduction]
red_one_brs [in MetaCoq.PCUIC.PCUICReduction]
red_one_context_decl_rel [in MetaCoq.PCUIC.PCUICReduction]
red_rect_1n [in MetaCoq.PCUIC.PCUICReduction]
red_rect_n1 [in MetaCoq.PCUIC.PCUICReduction]
red_rect' [in MetaCoq.PCUIC.PCUICReduction]
red_context_rel [in MetaCoq.PCUIC.PCUICReduction]
red_context [in MetaCoq.PCUIC.PCUICReduction]
red_ctx_rel [in MetaCoq.PCUIC.PCUICReduction]
red_one_ctx_rel [in MetaCoq.PCUIC.PCUICReduction]
red1P [in MetaCoq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_right [in MetaCoq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_ctx [in MetaCoq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_left [in MetaCoq.PCUIC.PCUICSubstitution]
red1P_red1 [in MetaCoq.PCUIC.PCUICSubstitution]
red1_rel_alpha [in MetaCoq.PCUIC.PCUICConfluence]
red1_rel [in MetaCoq.PCUIC.PCUICConfluence]
red1_red_ctxP [in MetaCoq.PCUIC.PCUICContextConversion]
red1_ctx_rel [in MetaCoq.PCUIC.PCUICReduction]
red1_ctx [in MetaCoq.PCUIC.PCUICReduction]
referenced_impl_sq_wf [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_pop [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
reflect_eq_predicate [in MetaCoq.SafeChecker.PCUICEqualityDec]
refresh_universes [in MetaCoq.Translations.times_bool_fun]
refresh_universes [in MetaCoq.Translations.param_cheap_packed]
refresh_universes [in MetaCoq.Translations.param_generous_packed]
reify [in MetaCoq.Examples.tauto]
reify_correct [in MetaCoq.Examples.tauto]
relation [in MetaCoq.Translations.MiniHoTT]
relation [in MetaCoq.Translations.MiniHoTT_paths]
reln_alt [in MetaCoq.PCUIC.utils.PCUICAstUtils]
remove_arity [in MetaCoq.PCUIC.utils.PCUICAstUtils]
remove_last [in MetaCoq.Template.utils.MCList]
remove_params_fast_optimization [in MetaCoq.Erasure.ETransform]
remove_params_optimization [in MetaCoq.Erasure.ETransform]
remove_arity [in MetaCoq.Template.AstUtils]
remove_last_n [in MetaCoq.Examples.add_constructor]
ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_telescope [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_decl [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_context [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_constructor_body [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_branch [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_decl [in MetaCoq.Template.Pretty]
rename_decl [in MetaCoq.PCUIC.utils.PCUICPretty]
renaming [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
renaming [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ren_ids [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_id [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_fn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
replace [in MetaCoq.Translations.times_bool_fun]
replace [in MetaCoq.Translations.param_cheap_packed]
Req [in MetaCoq.SafeChecker.PCUICSafeReduce]
Ret [in MetaCoq.SafeChecker.PCUICSafeConversion]
retract [in MetaCoq.Translations.times_bool_fun2]
rev [in MetaCoq.Template.utils.MCList]
rev_map [in MetaCoq.Template.utils.MCList]
rho [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ws_pair [in MetaCoq.PCUIC.PCUICConfluence]
rho_fix_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_wf [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rigid_head [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
rshiftk [in MetaCoq.PCUIC.PCUICSigmaCalculus]
run_erase_program_fast [in MetaCoq.Erasure.Erasure]
run_erase_program [in MetaCoq.Erasure.Erasure]
R_global_instance [in MetaCoq.Template.TermEquality]
R_opt_variance [in MetaCoq.Template.TermEquality]
R_universe_instance_variance [in MetaCoq.Template.TermEquality]
R_universe_variance [in MetaCoq.Template.TermEquality]
R_universe_instance [in MetaCoq.Template.TermEquality]
R_ind_universes [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance [in MetaCoq.PCUIC.PCUICEquality]
R_opt_variance [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_variance [in MetaCoq.PCUIC.PCUICEquality]
R_universe_variance [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance [in MetaCoq.PCUIC.PCUICEquality]
R_singleton [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_aux [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_aux [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_opt [in MetaCoq.Template.utils.MCOption]
R_opt [in MetaCoq.SafeChecker.PCUICSafeChecker]


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)