| 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 (definition)
R [in MetaRocq.SafeChecker.PCUICSafeReduce]R [in MetaRocq.SafeChecker.PCUICSafeConversion]
Raw.quote_wf_ext [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_wf [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_wf_local [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_red [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_typing [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_term [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_context [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_global_env_ext [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_checker_flags [in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_wf_ext [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_wf [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_wf_local [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_red [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_typing [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_term [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_context [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_global_env_ext [in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_checker_flags [in MetaRocq.Quotation.ToTemplate.All]
Raw.WfAst.quote_wf [in MetaRocq.Quotation.ToTemplate.All]
rebase_global_reference [in MetaRocq.Quotation.CommonUtils]
rebuild_wf_env_transform [in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env [in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
rebuild_case_branch_ctx [in MetaRocq.Template.Checker]
rebuild_case_predicate_ctx [in MetaRocq.Template.Checker]
recursivity_kind_sind [in MetaRocq.Common.BasicAst]
recursivity_kind_rec [in MetaRocq.Common.BasicAst]
recursivity_kind_ind [in MetaRocq.Common.BasicAst]
recursivity_kind_rect [in MetaRocq.Common.BasicAst]
red [in MetaRocq.PCUIC.PCUICReduction]
RedFlags.default [in MetaRocq.PCUIC.PCUICNormal]
RedFlags.default [in MetaRocq.Template.Checker]
RedFlags.nodelta [in MetaRocq.PCUIC.PCUICNormal]
redl_branch [in MetaRocq.PCUIC.PCUICReduction]
redl_context [in MetaRocq.PCUIC.PCUICReduction]
redl_term [in MetaRocq.PCUIC.PCUICReduction]
redl_sind [in MetaRocq.PCUIC.PCUICReduction]
redl_rec [in MetaRocq.PCUIC.PCUICReduction]
redl_ind [in MetaRocq.PCUIC.PCUICReduction]
redl_rect [in MetaRocq.PCUIC.PCUICReduction]
redp [in MetaRocq.SafeChecker.PCUICWfReduction]
redp_subterm_rel [in MetaRocq.SafeChecker.PCUICWfReduction]
reduce [in MetaRocq.Template.Checker]
reduce_to_ind [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_prod [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_sort [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_term [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_full [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_eq [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_stack_eq [in MetaRocq.Erasure.ErasureFunctionProperties]
reduce_to_ind [in MetaRocq.Template.Checker]
reduce_to_prod [in MetaRocq.Template.Checker]
reduce_to_sort [in MetaRocq.Template.Checker]
reduce_opt [in MetaRocq.Template.Checker]
reduce_stack_term [in MetaRocq.Template.Checker]
reduce_stack [in MetaRocq.Template.Checker]
reducible_head [in MetaRocq.Template.Checker]
reducible_head [in MetaRocq.SafeChecker.PCUICSafeConversion]
red_decls_sind [in MetaRocq.Erasure.Prelim]
red_decls_rec [in MetaRocq.Erasure.Prelim]
red_decls_ind [in MetaRocq.Erasure.Prelim]
red_decls_rect [in MetaRocq.Erasure.Prelim]
red_viewc [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_sind [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_rec [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_ind [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_rect [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_discr [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_ctx_alpha [in MetaRocq.PCUIC.PCUICConfluence]
red_rel_ctx [in MetaRocq.PCUIC.PCUICConfluence]
red_ctx [in MetaRocq.PCUIC.PCUICConfluence]
red_sind [in MetaRocq.Template.Typing]
red_rec [in MetaRocq.Template.Typing]
red_ind [in MetaRocq.Template.Typing]
red_rect [in MetaRocq.Template.Typing]
red_brs [in MetaRocq.PCUIC.PCUICReduction]
red_one_brs [in MetaRocq.PCUIC.PCUICReduction]
red_one_context_decl_rel [in MetaRocq.PCUIC.PCUICReduction]
red_rect_1n [in MetaRocq.PCUIC.PCUICReduction]
red_rect_n1 [in MetaRocq.PCUIC.PCUICReduction]
red_rect' [in MetaRocq.PCUIC.PCUICReduction]
red_context_rel [in MetaRocq.PCUIC.PCUICReduction]
red_context [in MetaRocq.PCUIC.PCUICReduction]
red_decls_sind [in MetaRocq.PCUIC.PCUICReduction]
red_decls_rec [in MetaRocq.PCUIC.PCUICReduction]
red_decls_ind [in MetaRocq.PCUIC.PCUICReduction]
red_decls_rect [in MetaRocq.PCUIC.PCUICReduction]
red_ctx_rel [in MetaRocq.PCUIC.PCUICReduction]
red_one_ctx_rel [in MetaRocq.PCUIC.PCUICReduction]
Red1Apps.red1_sind [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_rec [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_ind [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_rect [in MetaRocq.PCUIC.PCUICEtaExpand]
red1P [in MetaRocq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_right [in MetaRocq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_left [in MetaRocq.PCUIC.PCUICSubstitution]
red1P_red1 [in MetaRocq.PCUIC.PCUICSubstitution]
red1_red_ctxP [in MetaRocq.PCUIC.PCUICContextConversion]
red1_rel_alpha [in MetaRocq.PCUIC.PCUICConfluence]
red1_rel [in MetaRocq.PCUIC.PCUICConfluence]
red1_sind [in MetaRocq.Template.Typing]
red1_rec [in MetaRocq.Template.Typing]
red1_ind [in MetaRocq.Template.Typing]
red1_rect [in MetaRocq.Template.Typing]
red1_ctx_rel [in MetaRocq.PCUIC.PCUICReduction]
red1_ctx [in MetaRocq.PCUIC.PCUICReduction]
red1_sind [in MetaRocq.PCUIC.PCUICReduction]
red1_rec [in MetaRocq.PCUIC.PCUICReduction]
red1_ind [in MetaRocq.PCUIC.PCUICReduction]
red1_rect [in MetaRocq.PCUIC.PCUICReduction]
reference_impl_sq_wf [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_pop [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reflectProp_sind [in MetaRocq.Utils.ReflectEq]
reflectProp_ind [in MetaRocq.Utils.ReflectEq]
reflectT_sind [in MetaRocq.Utils.MRReflect]
reflectT_rec [in MetaRocq.Utils.MRReflect]
reflectT_ind [in MetaRocq.Utils.MRReflect]
reflectT_rect [in MetaRocq.Utils.MRReflect]
reify [in MetaRocq.Examples.tauto]
reify_correct [in MetaRocq.Examples.tauto]
reindex [in MetaRocq.Erasure.Typed.Optimize]
relevance_sind [in MetaRocq.Common.BasicAst]
relevance_rec [in MetaRocq.Common.BasicAst]
relevance_ind [in MetaRocq.Common.BasicAst]
relevance_rect [in MetaRocq.Common.BasicAst]
reln_alt [in MetaRocq.PCUIC.utils.PCUICAstUtils]
rel_option_sind [in MetaRocq.PCUIC.PCUICEquality]
rel_option_rec [in MetaRocq.PCUIC.PCUICEquality]
rel_option_ind [in MetaRocq.PCUIC.PCUICEquality]
rel_option_rect [in MetaRocq.PCUIC.PCUICEquality]
remove_last [in MetaRocq.Utils.MRList]
remove_arity [in MetaRocq.Template.AstUtils]
remove_last_n [in MetaRocq.Examples.add_constructor]
remove_match_on_box_env [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_match_on_box_decl [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_match_on_box_constant_body [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_var [in MetaRocq.Erasure.Typed.Optimize]
remove_vars [in MetaRocq.Erasure.Typed.Optimize]
remove_arity [in MetaRocq.PCUIC.utils.PCUICAstUtils]
remove_top_prod [in MetaRocq.Erasure.Typed.CertifyingEta]
remove_match_on_box_program_expanded_fix [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_program_expanded [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_program_wf [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_program [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env' [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_decl [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_constant_decl [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_trans [in MetaRocq.ErasurePlugin.ETransform]
remove_params_fast_optimization [in MetaRocq.ErasurePlugin.ETransform]
remove_params_optimization [in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_typed_transform [in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_program_typed [in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_typed_env [in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_typed_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
ren [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_decl [in MetaRocq.Template.Pretty]
rename_mfix [in MetaRocq.PCUIC.PCUICGuardCondition]
rename_decl [in MetaRocq.PCUIC.utils.PCUICPretty]
rename_constructor_body [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_branch [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_telescope [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_decl [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_context [in MetaRocq.PCUIC.PCUICSigmaCalculus]
renaming [in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
renaming [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
renamingT [in MetaRocq.PCUIC.PCUICSigmaCalculus]
renaming_closed [in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
ren_ids [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_id [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_fn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
reorder [in MetaRocq.Erasure.EReorderCstrs]
reorder_program_expanded_fix [in MetaRocq.Erasure.EReorderCstrs]
reorder_program_expanded [in MetaRocq.Erasure.EReorderCstrs]
reorder_program_wf [in MetaRocq.Erasure.EReorderCstrs]
reorder_program [in MetaRocq.Erasure.EReorderCstrs]
reorder_env [in MetaRocq.Erasure.EReorderCstrs]
reorder_decl [in MetaRocq.Erasure.EReorderCstrs]
reorder_inductive_decl [in MetaRocq.Erasure.EReorderCstrs]
reorder_one_ind [in MetaRocq.Erasure.EReorderCstrs]
reorder_constant_decl [in MetaRocq.Erasure.EReorderCstrs]
reorder_branches [in MetaRocq.Erasure.EReorderCstrs]
reorder_list [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt [in MetaRocq.Erasure.EReorderCstrs]
reorder_cstrs_transformation [in MetaRocq.ErasurePlugin.ETransform]
replace_inductive_modpath [in MetaRocq.Quotation.CommonUtils]
replace_inductive_kn [in MetaRocq.Quotation.CommonUtils]
replace_quotation_of [in MetaRocq.Quotation.ToPCUIC.Init]
replace_quotation_of' [in MetaRocq.Quotation.ToPCUIC.Init]
replace_quotation_of [in MetaRocq.Quotation.ToTemplate.Init]
replace_quotation_of' [in MetaRocq.Quotation.ToTemplate.Init]
replace_char [in MetaRocq.Erasure.Typed.Certifying]
represents_value_ind [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_ind [in MetaRocq.Erasure.EWcbvEvalNamed]
repr_decls [in MetaRocq.Template.EtaExpand]
rep_ind [in MetaRocq.Erasure.EWcbvEvalNamed]
Req [in MetaRocq.SafeChecker.PCUICSafeReduce]
restrict_env [in MetaRocq.Erasure.Typed.CertifyingEta]
result_sind [in MetaRocq.Examples.tauto]
result_rec [in MetaRocq.Examples.tauto]
result_ind [in MetaRocq.Examples.tauto]
result_rect [in MetaRocq.Examples.tauto]
result_sind [in MetaRocq.Erasure.Typed.ResultMonad]
result_rec [in MetaRocq.Erasure.Typed.ResultMonad]
result_ind [in MetaRocq.Erasure.Typed.ResultMonad]
result_rect [in MetaRocq.Erasure.Typed.ResultMonad]
Ret [in MetaRocq.SafeChecker.PCUICSafeConversion]
Retroknowledge.compatible [in MetaRocq.Common.Environment]
Retroknowledge.empty [in MetaRocq.Common.Environment]
Retroknowledge.extends [in MetaRocq.Common.Environment]
Retroknowledge.extendsb [in MetaRocq.Common.Environment]
Retroknowledge.merge [in MetaRocq.Common.Environment]
rev [in MetaRocq.Utils.MRList]
rev_map [in MetaRocq.Utils.MRList]
rev_mapi_length_app [in MetaRocq.Erasure.Typed.TypeAnnotations]
rho [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ws_pair [in MetaRocq.PCUIC.PCUICConfluence]
rho_fix_spec_sind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_rec [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_ind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_rect [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rigid_head [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
rshiftk [in MetaRocq.PCUIC.PCUICSigmaCalculus]
run_transforms [in MetaRocq.Erasure.Typed.Extraction]
run_transforms_list [in MetaRocq.Erasure.Typed.Extraction]
run_erase_program [in MetaRocq.ErasurePlugin.Erasure]
R_singleton [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_aux [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_opt [in MetaRocq.Utils.MROption]
R_opt [in MetaRocq.SafeChecker.PCUICSafeChecker]
R_aux [in MetaRocq.SafeChecker.PCUICSafeConversion]
| 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) |