| 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
R [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]R [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
raise [projection, in MetaRocq.Utils.monad_utils]
raise [abbreviation, in MetaRocq.SafeChecker.PCUICTypeChecker]
RandomLemmas [section, in MetaRocq.PCUIC.PCUICCasesHelper]
RandomLemmas.cf [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
rarg [projection, in MetaRocq.Common.BasicAst]
rarg [projection, in MetaRocq.Erasure.EAst]
Raw [module, in MetaRocq.Quotation.ToPCUIC.All]
Raw [module, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote [abbreviation, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote [abbreviation, in MetaRocq.Quotation.ToTemplate.All]
Raw.QuoteNotationHints [module, in MetaRocq.Quotation.ToPCUIC.All]
Raw.QuoteNotationHints [module, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_wf_ext [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_wf [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_wf_local [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_red [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_typing [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_term [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_context [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_global_env_ext [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_checker_flags [definition, in MetaRocq.Quotation.ToPCUIC.All]
Raw.quote_wf_ext [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_wf [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_wf_local [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_red [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_typing [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_term [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_context [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_global_env_ext [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.quote_checker_flags [definition, in MetaRocq.Quotation.ToTemplate.All]
Raw.WfAst [module, in MetaRocq.Quotation.ToTemplate.All]
Raw.WfAst.quote_wf [definition, in MetaRocq.Quotation.ToTemplate.All]
rebase_global_reference [definition, in MetaRocq.Quotation.CommonUtils]
rebuild_wf_env_transform_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
rebuild_wf_env_transform_pres_fo [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
rebuild_wf_env_irr [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
rebuild_wf_env_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env [definition, in MetaRocq.ErasurePlugin.ETransform]
rebuild_wf_env_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
rebuild_case_branch_ctx [definition, in MetaRocq.Template.Checker]
rebuild_case_predicate_ctx [definition, in MetaRocq.Template.Checker]
rec [abbreviation, in MetaRocq.SafeChecker.PCUICSafeReduce]
recomp_branch' [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
recomp_branch [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
recursivity_kind_sind [definition, in MetaRocq.Common.BasicAst]
recursivity_kind_rec [definition, in MetaRocq.Common.BasicAst]
recursivity_kind_ind [definition, in MetaRocq.Common.BasicAst]
recursivity_kind_rect [definition, in MetaRocq.Common.BasicAst]
recursivity_kind [inductive, in MetaRocq.Common.BasicAst]
red [inductive, in MetaRocq.Template.Typing]
red [definition, in MetaRocq.PCUIC.PCUICReduction]
RedConfluence [section, in MetaRocq.PCUIC.PCUICConfluence]
RedConfluence.cf [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedConfluence.wfΣ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedConfluence.Σ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedConv [section, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
RedConv.cf [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
RedConv.wfΣ [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
RedConv.Σ [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
RedEq [section, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext [section, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.cmp_sort [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.cmp_universe [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.hsubst_sort_pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.hsubst_sort_conv [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.hsubst_univ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.preorder_sort_pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.preorder_sort_conv [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.preorder_univ_pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.preorder_univ_conv [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.sub_sort [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.sub_univ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEqContext.Σ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.cmp_sort [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.cmp_universe [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.hsubst_sort_pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.hsubst_sort_conv [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.hsubst_univ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.preorder_sort_pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.preorder_sort_conv [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.preorder_univ_pb [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.preorder_univ_conv [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.sub_sort [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.sub_univ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedEq.Σ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedFlags [module, in MetaRocq.PCUIC.PCUICNormal]
RedFlags [module, in MetaRocq.Template.Checker]
RedFlags.beta [projection, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.beta [projection, in MetaRocq.Template.Checker]
RedFlags.cofix_ [projection, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.cofix_ [projection, in MetaRocq.Template.Checker]
RedFlags.default [definition, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.default [definition, in MetaRocq.Template.Checker]
RedFlags.delta [projection, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.delta [projection, in MetaRocq.Template.Checker]
RedFlags.fix_ [projection, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.fix_ [projection, in MetaRocq.Template.Checker]
RedFlags.iota [projection, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.iota [projection, in MetaRocq.Template.Checker]
RedFlags.nodelta [definition, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.t [record, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.t [record, in MetaRocq.Template.Checker]
RedFlags.zeta [projection, in MetaRocq.PCUIC.PCUICNormal]
RedFlags.zeta [projection, in MetaRocq.Template.Checker]
redl [inductive, in MetaRocq.PCUIC.PCUICReduction]
redl_context_trans [lemma, in MetaRocq.PCUIC.PCUICReduction]
redl_context_impl [lemma, in MetaRocq.PCUIC.PCUICReduction]
redl_branch [definition, in MetaRocq.PCUIC.PCUICReduction]
redl_context [definition, in MetaRocq.PCUIC.PCUICReduction]
redl_term [definition, in MetaRocq.PCUIC.PCUICReduction]
redl_preserve [lemma, in MetaRocq.PCUIC.PCUICReduction]
redl_sind [definition, in MetaRocq.PCUIC.PCUICReduction]
redl_rec [definition, in MetaRocq.PCUIC.PCUICReduction]
redl_ind [definition, in MetaRocq.PCUIC.PCUICReduction]
redl_rect [definition, in MetaRocq.PCUIC.PCUICReduction]
redp [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
RedPred [section, in MetaRocq.PCUIC.PCUICConfluence]
RedPred.cf [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedPred.wfΣ [variable, in MetaRocq.PCUIC.PCUICConfluence]
RedPred.Σ [variable, in MetaRocq.PCUIC.PCUICConfluence]
redp_subterm_rel [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
redp_red [instance, in MetaRocq.SafeChecker.PCUICWfReduction]
redp_trans [instance, in MetaRocq.SafeChecker.PCUICWfReduction]
Reduce [section, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce [definition, in MetaRocq.Template.Checker]
Reduce [section, in MetaRocq.Template.Checker]
reduced_proj_body_whne [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
reduced_case_discriminee_whne [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
ReduceFns [section, in MetaRocq.SafeChecker.PCUICSafeReduce]
ReduceFns.cf [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
ReduceFns.no [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
ReduceFns.normalization_in [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
ReduceFns.X [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
ReduceFns.X_type [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_ind_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_ind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_prod_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_prod [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_sort_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_sort [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_term_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_whnf [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_prop [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_term_sound [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_term [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_noLamApp [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_noApp [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_isred [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_context [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_decompose [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_sound [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_Req [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_full [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_ind_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_sort_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_prod_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_stack_eq [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_stack_eq [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
reduce_to_ind [definition, in MetaRocq.Template.Checker]
reduce_to_prod [definition, in MetaRocq.Template.Checker]
reduce_to_sort [definition, in MetaRocq.Template.Checker]
reduce_opt [definition, in MetaRocq.Template.Checker]
reduce_stack_term [definition, in MetaRocq.Template.Checker]
reduce_stack [definition, in MetaRocq.Template.Checker]
Reduce.cf [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.flags [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.flags [variable, in MetaRocq.Template.Checker]
Reduce.no [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.normalization_in [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.reducewf [section, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.reducewf.Γ [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.X [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.X_type [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Reduce.Σ [variable, in MetaRocq.Template.Checker]
reducible_head [definition, in MetaRocq.Template.Checker]
reducible_head_None [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_decompose [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_cored [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zippx [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zipp [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
Reduction [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
Reduction [library]
ReductionCongruence [section, in MetaRocq.PCUIC.PCUICReduction]
ReductionCongruence.Congruences [section, in MetaRocq.PCUIC.PCUICReduction]
ReductionCongruence.Congruences.Γ [variable, in MetaRocq.PCUIC.PCUICReduction]
ReductionCongruence.FillContext [section, in MetaRocq.PCUIC.PCUICReduction]
ReductionCongruence.FillContext.t [variable, in MetaRocq.PCUIC.PCUICReduction]
ReductionCongruence.Σ [variable, in MetaRocq.PCUIC.PCUICReduction]
reductionStrategy [inductive, in MetaRocq.Template.TemplateMonad.Common]
red_terms_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICNormal]
red_ctx_rel_subst [lemma, in MetaRocq.PCUIC.PCUICNormal]
red_it_mkProd_or_LetIn_smash_context [lemma, in MetaRocq.Erasure.Typed.Erasure]
red_conv_conv_inv [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_conv_conv [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_conv [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul_cumul_inv [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul_cumul [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul_inv [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
red_ctx_app_context_l [lemma, in MetaRocq.PCUIC.PCUICSR]
red_ctx_clos_rt_red1_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
red_terms_refl [lemma, in MetaRocq.PCUIC.PCUICSR]
red_one_decl_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICSR]
red_one_decl_red_context [lemma, in MetaRocq.PCUIC.PCUICSR]
red_one_decl_red_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
red_context [abbreviation, in MetaRocq.Erasure.Prelim]
red_decls_sind [definition, in MetaRocq.Erasure.Prelim]
red_decls_rec [definition, in MetaRocq.Erasure.Prelim]
red_decls_ind [definition, in MetaRocq.Erasure.Prelim]
red_decls_rect [definition, in MetaRocq.Erasure.Prelim]
red_decls [inductive, in MetaRocq.Erasure.Prelim]
red_viewc [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_sind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_rec [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_ind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_rect [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_other [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Proj [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Case [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Fix [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Lambda [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_App [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Const [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_LetIn [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view_Rel [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_view [inductive, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_discr [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_welltyped [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
red_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
red_letin_alt [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
red_abs_alt [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
red_expand_let [lemma, in MetaRocq.PCUIC.PCUICSpine]
red_zipc [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
red_cored_cored [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
red_welltyped [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
red_neq_cored [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
red_const [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
red_cored_or_eq [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
red_ws_cumul_pb_inv [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_right [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_left [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_conv [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_is_open_term [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_decl_refl [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx_inv' [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_compare_term_r [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_compare_term_l [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_closed_right [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_closed_left [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars_term [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx_aux' [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx' [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_app [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_skip [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red_confluence [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ws_red_left [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tConst_axiom [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tRel [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tInd [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tConstruct [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_red_ctx_alpha_trans [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_alpha_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_alpha [definition, in MetaRocq.PCUIC.PCUICConfluence]
red_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_context_trans [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_red_context [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ws_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_clos_rt_red1_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
red_rel_ctx [definition, in MetaRocq.PCUIC.PCUICConfluence]
red_trans_clos_pred1 [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_ctx [definition, in MetaRocq.PCUIC.PCUICConfluence]
red_pred [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_pred' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_eq_context_upto_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_eq_context_upto_l [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_l [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red_Trans [instance, in MetaRocq.PCUIC.PCUICConfluence]
red_Refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
red_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_conv_extended_subst [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_terms_lift [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_assumptions [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_subst_instance [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
red_betas_typed [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_betas [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_betas0 [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_terms_evar [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_rel_all [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_fix_or_cofix_body [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_terms_refl [instance, in MetaRocq.PCUIC.PCUICConversion]
red_brs_refl [instance, in MetaRocq.PCUIC.PCUICConversion]
red_terms_ws_cumul_pb_terms [lemma, in MetaRocq.PCUIC.PCUICConversion]
red_terms [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
red_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
red_on_free_vars [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
red_vdefs_tProd [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
red_ctx_rel_red_context_rel [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_rel_inv [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app_right [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_trans [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_rel_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app_same_left [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app_same [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_context_refl [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_decls_refl [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_prod_alt [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red_sind [definition, in MetaRocq.Template.Typing]
red_rec [definition, in MetaRocq.Template.Typing]
red_ind [definition, in MetaRocq.Template.Typing]
red_rect [definition, in MetaRocq.Template.Typing]
red_proj [constructor, in MetaRocq.Template.Typing]
red_delta [constructor, in MetaRocq.Template.Typing]
red_cofix_proj [constructor, in MetaRocq.Template.Typing]
red_cofix_case [constructor, in MetaRocq.Template.Typing]
red_fix [constructor, in MetaRocq.Template.Typing]
red_iota [constructor, in MetaRocq.Template.Typing]
red_rel [constructor, in MetaRocq.Template.Typing]
red_zeta [constructor, in MetaRocq.Template.Typing]
red_beta [constructor, in MetaRocq.Template.Typing]
red_it_mkProd_or_LetIn_mkApps_Ind [lemma, in MetaRocq.PCUIC.PCUICInductives]
red_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICInductives]
red_destInd [lemma, in MetaRocq.PCUIC.PCUICInductives]
red_zippx [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_zipp [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_context_zip [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_atom [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_evar [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_one_evar [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_prod [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_prod_r [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_prod_l [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_primArray_congr [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_primArray_type [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_primArray_default [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_primArray_value [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_primArray_one_value [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_congr [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_body [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_one_body [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_ty [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_one_ty [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_fix_congr [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_fix_body [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_fix_one_body [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_fix_ty [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_fix_one_ty [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_proj_c [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_case [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_case_brs [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_one_brs_red_brs [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_brs [definition, in MetaRocq.PCUIC.PCUICReduction]
red_one_brs [definition, in MetaRocq.PCUIC.PCUICReduction]
red_case_one_brs [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_case_c [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_case_p [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_case_pars [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_one_param [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_letin [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_mkApps [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_mkApps_f [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_app [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_app_r [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_abs [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_one_decl_red_ctx_rel [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_one_context_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_one_branch [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
red_one_context_decl [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
red_one_context_decl_rel [definition, in MetaRocq.PCUIC.PCUICReduction]
red_one_term [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
red_ctx_congr [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_contextual_closure_equiv [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_contextual_closure [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_trans [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_step [lemma, in MetaRocq.PCUIC.PCUICReduction]
red_rect_1n [definition, in MetaRocq.PCUIC.PCUICReduction]
red_rect_n1 [definition, in MetaRocq.PCUIC.PCUICReduction]
red_rect' [definition, in MetaRocq.PCUIC.PCUICReduction]
red_context_rel [definition, in MetaRocq.PCUIC.PCUICReduction]
red_context [definition, in MetaRocq.PCUIC.PCUICReduction]
red_decls_sind [definition, in MetaRocq.PCUIC.PCUICReduction]
red_decls_rec [definition, in MetaRocq.PCUIC.PCUICReduction]
red_decls_ind [definition, in MetaRocq.PCUIC.PCUICReduction]
red_decls_rect [definition, in MetaRocq.PCUIC.PCUICReduction]
red_vdef_body [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_vass [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_decls [inductive, in MetaRocq.PCUIC.PCUICReduction]
red_ctx_rel [definition, in MetaRocq.PCUIC.PCUICReduction]
red_one_ctx_rel [definition, in MetaRocq.PCUIC.PCUICReduction]
red_proj [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_delta [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_proj [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_cofix_case [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_fix [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_iota [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_rel [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_zeta [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_beta [constructor, in MetaRocq.PCUIC.PCUICReduction]
red_cumul_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
red_conv_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
red_upto_conv_ctx_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
red_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICClassification]
red_ctx_rel_par_conv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
red_case_isproof [lemma, in MetaRocq.Erasure.EArities]
red_conv_cum_r [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
red_conv_cum_l [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
red_brs_refl [instance, in MetaRocq.SafeChecker.PCUICSafeConversion]
red_on_free_vars [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
red1 [inductive, in MetaRocq.Template.Typing]
red1 [inductive, in MetaRocq.PCUIC.PCUICReduction]
Red1Apps [module, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.abs_red_r [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.abs_red_l [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_fix_red_body [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_fix_red_ty [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_red_r [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.app_red_l [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.array_red_type [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.array_red_def [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.array_red_val [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_brs [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_discr [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_return [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.case_red_param [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.cofix_red_body [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.cofix_red_ty [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.evar_red [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.fix_red_body [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.fix_red_ty [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.isLambda_red1 [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.letin_red_body [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.letin_red_ty [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.letin_red_def [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.prod_red_r [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.prod_red_l [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.proj_red [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_tApp [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_proj [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_delta [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_cofix_proj [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_cofix_case [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_fix [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_iota [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_rel [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_zeta [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_beta [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1 [inductive, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_ind_all [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_sind [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_rec [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_ind [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_rect [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
_ ;;; _ |- _ ⇝ _ [notation, in MetaRocq.PCUIC.PCUICEtaExpand]
red1P [definition, in MetaRocq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_right [definition, in MetaRocq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_ctx [definition, in MetaRocq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_left [definition, in MetaRocq.PCUIC.PCUICSubstitution]
red1P_red1 [definition, in MetaRocq.PCUIC.PCUICSubstitution]
red1_mkApps_tCoFix_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_tFix_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_tInd_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_tConstruct_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_r [lemma, in MetaRocq.Template.Reduction]
red1_mkApps_l [lemma, in MetaRocq.Template.Reduction]
red1_mkApp [lemma, in MetaRocq.Template.Reduction]
red1_tApp_mkApp [lemma, in MetaRocq.Template.Reduction]
red1_tApp_mkApps_l [lemma, in MetaRocq.Template.Reduction]
red1_red_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
red1_ctx_app [lemma, in MetaRocq.PCUIC.PCUICSR]
red1_it_mkLambda_or_LetIn_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
red1_is_open_term [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red1_red_ctx_aux [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red1_red_ctxP_app [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
red1_red_ctxP [definition, in MetaRocq.PCUIC.PCUICContextConversion]
red1_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel_inv [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha_pred1_rel_alpha [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha [definition, in MetaRocq.PCUIC.PCUICConfluence]
red1_ctx_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_ctx_pred1_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_rel [definition, in MetaRocq.PCUIC.PCUICConfluence]
red1_weak_confluence [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_pred1 [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_l [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_univ_l [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_l [lemma, in MetaRocq.PCUIC.PCUICConfluence]
red1_ctx_rel [abbreviation, in MetaRocq.PCUIC.PCUICConfluence]
red1_conv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumulSpec [lemma, in MetaRocq.PCUIC.PCUICConversion]
red1_red1apps [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
red1_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
red1_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
red1_ind_all [lemma, in MetaRocq.Template.Typing]
red1_sind [definition, in MetaRocq.Template.Typing]
red1_rec [definition, in MetaRocq.Template.Typing]
red1_ind [definition, in MetaRocq.Template.Typing]
red1_rect [definition, in MetaRocq.Template.Typing]
red1_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICInductives]
red1_destInd [lemma, in MetaRocq.PCUIC.PCUICInductives]
red1_zippx [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_zipp [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_context [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_fill_context_hole [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_mkApps_r [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_mkApps_f [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_one_branch [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
red1_one_context_decl [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
red1_one_term [abbreviation, in MetaRocq.PCUIC.PCUICReduction]
red1_red [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_ind_all [lemma, in MetaRocq.PCUIC.PCUICReduction]
red1_ctx_rel [definition, in MetaRocq.PCUIC.PCUICReduction]
red1_ctx [definition, in MetaRocq.PCUIC.PCUICReduction]
red1_sind [definition, in MetaRocq.PCUIC.PCUICReduction]
red1_rec [definition, in MetaRocq.PCUIC.PCUICReduction]
red1_ind [definition, in MetaRocq.PCUIC.PCUICReduction]
red1_rect [definition, in MetaRocq.PCUIC.PCUICReduction]
red1_upto_conv_ctx_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
red1_isLambda [lemma, in MetaRocq.Template.TypingWf]
red1_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
red1_alpha_eq [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_conv [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_cumul_inv [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_cumul [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
red1_on_free_vars [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
reference_impl_env_iter_pop_eq [lemma, in MetaRocq.ErasurePlugin.ETransform]
reference_impl_env_iter_pop_eq' [lemma, in MetaRocq.ErasurePlugin.ETransform]
reference_impl_sq_wf [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_pop_decls_correct [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_pop [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_graph_wf [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_graph [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_wf [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_env [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl [record, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_ext_graph_wf [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_ext_graph [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_ext_wf [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_env_ext [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
reference_impl_ext [record, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
refine_red1_Γ [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
refine_red1_r [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
refine_pred [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
refine_red1_Γ [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
refine_red1_r [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
refine_red1_Γ [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
refine_red1_r [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Reflect [library]
ReflectAst [library]
reflectContext [section, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.cmps [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.cmpu [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.cmp_sort [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.cmp_universe [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.gen_compare_global_instance [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.hglobal [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.hglobal' [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.hs [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.hs' [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.hu [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.hu' [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.p [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.pb [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.q [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectContext.Σ [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
ReflectEq [record, in MetaRocq.Utils.ReflectEq]
ReflectEq [library]
ReflectEq_term [instance, in MetaRocq.Erasure.EReflect]
ReflectEq_of_listable [instance, in MetaRocq.Utils.MRListable]
reflectEq_andb_right [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_left [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_3 [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
ReflectEq_EqDec [instance, in MetaRocq.Utils.ReflectEq]
ReflectF [constructor, in MetaRocq.Utils.MRReflect]
reflectF [constructor, in MetaRocq.Utils.ReflectEq]
reflectP [constructor, in MetaRocq.Utils.ReflectEq]
reflectProp [inductive, in MetaRocq.Utils.ReflectEq]
reflectProp_sigma_simpl [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_noConfusion [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_equiv [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_reflect [lemma, in MetaRocq.Utils.ReflectEq]
reflectProp_sind [definition, in MetaRocq.Utils.ReflectEq]
reflectProp_ind [definition, in MetaRocq.Utils.ReflectEq]
ReflectT [constructor, in MetaRocq.Utils.MRReflect]
reflectT [inductive, in MetaRocq.Utils.MRReflect]
reflectT_change_left4 [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectT_change_left3 [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectT_change_left2 [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectT_pred2 [lemma, in MetaRocq.Utils.MRReflect]
reflectT_pred [lemma, in MetaRocq.Utils.MRReflect]
reflectT_subrelation' [lemma, in MetaRocq.Utils.MRReflect]
reflectT_subrelation [lemma, in MetaRocq.Utils.MRReflect]
reflectT_change_left [lemma, in MetaRocq.Utils.MRReflect]
reflectT_reflect [lemma, in MetaRocq.Utils.MRReflect]
reflectT_sind [definition, in MetaRocq.Utils.MRReflect]
reflectT_rec [definition, in MetaRocq.Utils.MRReflect]
reflectT_ind [definition, in MetaRocq.Utils.MRReflect]
reflectT_rect [definition, in MetaRocq.Utils.MRReflect]
reflectT_forallb [lemma, in MetaRocq.Erasure.EPrimitive]
reflect_equiv [lemma, in MetaRocq.Utils.ByteCompareSpec]
reflect_global_decl [instance, in MetaRocq.Erasure.EReflect]
reflect_mutual_inductive_body [instance, in MetaRocq.Erasure.EReflect]
reflect_one_inductive_body [instance, in MetaRocq.Erasure.EReflect]
reflect_projection_body [instance, in MetaRocq.Erasure.EReflect]
reflect_constructor_body [instance, in MetaRocq.Erasure.EReflect]
reflect_constant_body [instance, in MetaRocq.Erasure.EReflect]
reflect_stack [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
reflect_choice [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
reflect_eq_term [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_leq_term [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eqb_termp_napp [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eqb_ctx_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eqb_decl_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eq_term_upto_univ [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eq_context_upto_names [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eq_decl_upto_names [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_global_instance [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_global_instance' [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_universe_instance_variance [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_universe_instance [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_Variance [instance, in MetaRocq.Common.Reflect]
reflect_allowed_eliminations [instance, in MetaRocq.Common.Reflect]
reflect_universes_decl [instance, in MetaRocq.Common.Reflect]
reflect_ConstraintType [instance, in MetaRocq.Common.Reflect]
reflect_recursivity_kind [instance, in MetaRocq.Common.Reflect]
reflect_case_info [instance, in MetaRocq.Common.Reflect]
reflect_cast_kind [instance, in MetaRocq.Common.Reflect]
reflect_def [instance, in MetaRocq.Common.Reflect]
reflect_aname [instance, in MetaRocq.Common.Reflect]
reflect_relevance [instance, in MetaRocq.Common.Reflect]
reflect_name [instance, in MetaRocq.Common.Reflect]
reflect_levels [instance, in MetaRocq.Common.Reflect]
reflect_prop_level [instance, in MetaRocq.Common.Reflect]
reflect_prim_float [instance, in MetaRocq.Common.Reflect]
reflect_prim_int [instance, in MetaRocq.Common.Reflect]
reflect_reflectT [lemma, in MetaRocq.Utils.MRReflect]
reflect_option_default [lemma, in MetaRocq.Utils.MROption]
reflect_global_decl [instance, in MetaRocq.Template.ReflectAst]
reflect_mutual_inductive_body [instance, in MetaRocq.Template.ReflectAst]
reflect_one_inductive_body [instance, in MetaRocq.Template.ReflectAst]
reflect_projection_body [instance, in MetaRocq.Template.ReflectAst]
reflect_constructor_body [instance, in MetaRocq.Template.ReflectAst]
reflect_constant_body [instance, in MetaRocq.Template.ReflectAst]
reflect_term [instance, in MetaRocq.Template.ReflectAst]
reflect_eq_projection [instance, in MetaRocq.Common.Kernames]
reflect_eq_inductive [instance, in MetaRocq.Common.Kernames]
reflect_global_decl [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_mutual_inductive_body [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_one_inductive_body [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_projection_body [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_constructor_body [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_constant_body [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_eq_predicate [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_prop_context_decl [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_prop_list [lemma, in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_prod [instance, in MetaRocq.Utils.ReflectEq]
reflect_sig_true [instance, in MetaRocq.Utils.ReflectEq]
reflect_bool [instance, in MetaRocq.Utils.ReflectEq]
reflect_nat [instance, in MetaRocq.Utils.ReflectEq]
reflect_list [instance, in MetaRocq.Utils.ReflectEq]
reflect_option [instance, in MetaRocq.Utils.ReflectEq]
reflect_reflectProp_2 [lemma, in MetaRocq.Utils.ReflectEq]
reflect_reflectProp_1 [lemma, in MetaRocq.Utils.ReflectEq]
reflect_reflectProp [lemma, in MetaRocq.Utils.ReflectEq]
reflect_eq_pstring [instance, in MetaRocq.Erasure.EPrimitive]
reflect_eq_array [instance, in MetaRocq.Erasure.EPrimitive]
reflect_eq_Z [instance, in MetaRocq.Erasure.EPrimitive]
reflect_eq_pstring [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_array [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_spec_float [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_uint63 [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
reflect_eq_Z [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
refl_red [constructor, in MetaRocq.Template.Typing]
refl_redl [constructor, in MetaRocq.PCUIC.PCUICReduction]
refl_red [lemma, in MetaRocq.PCUIC.PCUICReduction]
refl_eq_univ_prop [instance, in MetaRocq.PCUIC.PCUICCumulProp]
reify [definition, in MetaRocq.Examples.tauto]
reify_correct [definition, in MetaRocq.Examples.tauto]
reindex [definition, in MetaRocq.Erasure.Typed.Optimize]
relation_disjunction_Symmetric [instance, in MetaRocq.Utils.MRRelations]
relation_disjunction_refl_r [instance, in MetaRocq.Utils.MRRelations]
relation_disjunction_refl_l [instance, in MetaRocq.Utils.MRRelations]
relation_equivalence_inclusion [lemma, in MetaRocq.Utils.MRRelations]
relevance [inductive, in MetaRocq.Common.BasicAst]
relevance_sind [definition, in MetaRocq.Common.BasicAst]
relevance_rec [definition, in MetaRocq.Common.BasicAst]
relevance_ind [definition, in MetaRocq.Common.BasicAst]
relevance_rect [definition, in MetaRocq.Common.BasicAst]
Relevant [constructor, in MetaRocq.Common.BasicAst]
RelInductive [constructor, in MetaRocq.Erasure.Typed.Erasure]
reln_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICSR]
reln_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
reln_alt_eq [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_alt [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_list_lift_above [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_length [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_lift [lemma, in MetaRocq.PCUIC.PCUICContexts]
reln_acc [lemma, in MetaRocq.PCUIC.PCUICContexts]
reln_app [lemma, in MetaRocq.PCUIC.PCUICContexts]
RelOther [constructor, in MetaRocq.Erasure.Typed.Erasure]
RelTypeVar [constructor, in MetaRocq.Erasure.Typed.Erasure]
rel_option_sind [definition, in MetaRocq.PCUIC.PCUICEquality]
rel_option_rec [definition, in MetaRocq.PCUIC.PCUICEquality]
rel_option_ind [definition, in MetaRocq.PCUIC.PCUICEquality]
rel_option_rect [definition, in MetaRocq.PCUIC.PCUICEquality]
rel_none [constructor, in MetaRocq.PCUIC.PCUICEquality]
rel_some [constructor, in MetaRocq.PCUIC.PCUICEquality]
rel_option [inductive, in MetaRocq.PCUIC.PCUICEquality]
removelast_length [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
remove_last_last [lemma, in MetaRocq.Utils.MRList]
remove_last_app [lemma, in MetaRocq.Utils.MRList]
remove_last [definition, in MetaRocq.Utils.MRList]
remove_arity [definition, in MetaRocq.Template.AstUtils]
remove_last_n [definition, in MetaRocq.Examples.add_constructor]
remove_match_on_box_correct [lemma, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_match_on_box_env [definition, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_match_on_box_decl [definition, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_match_on_box_constant_body [definition, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_var [definition, in MetaRocq.Erasure.Typed.Optimize]
remove_vars [definition, in MetaRocq.Erasure.Typed.Optimize]
remove_arity [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
remove_params_optimization_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_params_optimization_pres [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_match_on_box_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_match_on_box_pres [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
remove_top_prod [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
remove_match_on_box_trans_env [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
remove_match_on_box_env_lemma [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
remove_match_on_box_program_expanded_fix [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_expanded_fix [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix_decl_irrel [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix_decl [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix_irrel [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_program_expanded [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_program_wf [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_program [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_wf [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_decl_wf [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_wellformed_decl_irrel [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_expanded [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_eq [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_extends_env [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_extends' [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_wellformed_irrel [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_wellformed [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_decl_irrel [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_decl [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_irrel [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_correct [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env' [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_decl [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_constant_decl [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_nth [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_cunfold_cofix [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_cunfold_fix [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_cofix_subst [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_fix_subst [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_iota_red [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_substl [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_csubst [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_mkApps [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box [definition, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box.Σ [variable, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box [section, in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_trans [definition, in MetaRocq.ErasurePlugin.ETransform]
remove_params_fast_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
remove_params_fast_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
remove_params_fast_optimization [definition, in MetaRocq.ErasurePlugin.ETransform]
remove_params_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
remove_params_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
remove_params_optimization [definition, in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_typed_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_program_typed [definition, in MetaRocq.ErasurePlugin.ETransform]
remove_match_on_box_typed_env [definition, in MetaRocq.ErasurePlugin.ETransform]
remove_last_length' [lemma, in MetaRocq.Erasure.EWcbvEval]
remove_last_length [lemma, in MetaRocq.Erasure.EWcbvEval]
remove_match_on_box_typed_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
ren [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_telescope [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
rename_decl [definition, in MetaRocq.Template.Pretty]
rename_context_on_free_vars [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_on_free_vars [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_ext_cond [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_mfix [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
rename_prim_type [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_cons [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_shiftn0 [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_ext [instance, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_subst_telescope [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_cofixpoint [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_fixpoint [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_cofix [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_fix [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_smash_context [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_app_context [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_decompose_prod_assum [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_predicate_preturn [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_case_branch_type [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_case_predicate_context [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_ind_predicate_context [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_decl [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
rename_iota_red [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_extended_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_preturn [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_pparams [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_compose [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branches [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branch [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_predicate [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_constructor_body [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_case_branch_context_gen [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_branch_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context_wf [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_set_binder_name [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_to_extended_list [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_reln [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_args [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_k [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_ext [instance, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_inds [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_shiftnk [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_constructor_body [definition, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_cofix [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_fix [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_branch [definition, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_extended_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_terms [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_decl [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_fix_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_decl_body [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_nth_error [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst10 [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_telescope [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_alt [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_mkApps [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_length [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose3 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose2 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose1 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_idsn_idsn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_inst_assoc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_ren_id [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_inst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_shiftn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branches_rename_branches [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branch_rename_branch [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_predicate_rename_predicate [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_compose [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branch_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_predicate_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_proper_pointwise [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branch [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_ext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_telescope [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_decl [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_context [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branches [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_predicate [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_context_lift_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
rename_rho_iota_red [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx_over [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rename_context_inst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
rename_decl_inst_decl [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
Renaming [section, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
renaming [definition, in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
Renaming [section, in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
Renaming [section, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
renaming [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
renamingT [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
renaming_vdef [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
renaming_vass [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
renaming_closed [definition, in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
renaming_extP [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
renaming_shift_rho_fix_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
renaming_ext [instance, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Renaming.cf [variable, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
Renaming.cf [variable, in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
Renaming.cf [variable, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
Renaming2 [section, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
Renaming2.cf [variable, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
ren_lift_renaming [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_subst_consn_comm [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_rshiftk [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_shiftk [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_idsn_consn_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_ids_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_ids_length [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_ids [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_consn_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_id_ids [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_id [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_shiftn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_ext [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_fn [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
reorder [abbreviation, in MetaRocq.Erasure.EReorderCstrs]
reorder [definition, in MetaRocq.Erasure.EReorderCstrs]
Reorder [section, in MetaRocq.Erasure.EReorderCstrs]
reorder_program_expanded_fix [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_program_expanded [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_program_wf [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_env_wf [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_env_expanded_fix [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_env_expanded [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_env [abbreviation, in MetaRocq.Erasure.EReorderCstrs]
reorder_decl [abbreviation, in MetaRocq.Erasure.EReorderCstrs]
reorder_mapping.wfm [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_mapping.Σ [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_mapping.mapping [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_mapping.wca [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_mapping.efl [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_mapping [section, in MetaRocq.Erasure.EReorderCstrs]
reorder_branches_map [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_map [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_proofs.wca [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_proofs.efl [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_length [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_proofs.wfm [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_proofs.m [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_proofs.Σ [variable, in MetaRocq.Erasure.EReorderCstrs]
reorder_proofs [section, in MetaRocq.Erasure.EReorderCstrs]
reorder_program [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_env [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_decl [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_inductive_decl [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_one_ind [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_constant_decl [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_branches [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_old_tag [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_spec_inv [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_spec' [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_spec' [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_In [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_spec [lemma, in MetaRocq.Erasure.EReorderCstrs]
reorder_list [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt [definition, in MetaRocq.Erasure.EReorderCstrs]
reorder_cstrs_transformation_ext' [instance, in MetaRocq.ErasurePlugin.ETransform]
reorder_cstrs_transformation_ext [instance, in MetaRocq.ErasurePlugin.ETransform]
reorder_cstrs_transformation [definition, in MetaRocq.ErasurePlugin.ETransform]
Reorder.mapping [variable, in MetaRocq.Erasure.EReorderCstrs]
Reorder.Σ [variable, in MetaRocq.Erasure.EReorderCstrs]
repack [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
repeat_snoc [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
replace_inductive_modpath [definition, in MetaRocq.Quotation.CommonUtils]
replace_inductive_kn [definition, in MetaRocq.Quotation.CommonUtils]
replace_quotation_of [definition, in MetaRocq.Quotation.ToPCUIC.Init]
replace_quotation_of' [definition, in MetaRocq.Quotation.ToPCUIC.Init]
replace_quotation_of [definition, in MetaRocq.Quotation.ToTemplate.Init]
replace_quotation_of' [definition, in MetaRocq.Quotation.ToTemplate.Init]
replace_char [definition, in MetaRocq.Erasure.Typed.Certifying]
represents [inductive, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_substl_rev [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_substl [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_subst_ctx [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_subst [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_subst' [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_bound_head [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_ind [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_ind [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tLazy [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tPrim [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tFix [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tConstruct [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value_tClos [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_value [inductive, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tForce [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tLazy [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tPrim [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tFix [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tCase [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tConstruct [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tConst [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tApp [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tLetIn [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_tLambda [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_unbound_tRel [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
represents_bound_tRel [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
repr_global_env_map [lemma, in MetaRocq.Template.EtaExpand]
repr_lookup_constructor [lemma, in MetaRocq.Template.EtaExpand]
repr_decls [definition, in MetaRocq.Template.EtaExpand]
rep_ind [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
Req [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
Req_red [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
Req_refl [instance, in MetaRocq.SafeChecker.PCUICSafeReduce]
Req_trans [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
restrict_env [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
result [inductive, in MetaRocq.Examples.tauto]
result [inductive, in MetaRocq.Erasure.Typed.ResultMonad]
ResultMonad [library]
result_sind [definition, in MetaRocq.Examples.tauto]
result_rec [definition, in MetaRocq.Examples.tauto]
result_ind [definition, in MetaRocq.Examples.tauto]
result_rect [definition, in MetaRocq.Examples.tauto]
result_sind [definition, in MetaRocq.Erasure.Typed.ResultMonad]
result_rec [definition, in MetaRocq.Erasure.Typed.ResultMonad]
result_ind [definition, in MetaRocq.Erasure.Typed.ResultMonad]
result_rect [definition, in MetaRocq.Erasure.Typed.ResultMonad]
ret [abbreviation, in MetaRocq.SafeChecker.PCUICSafeRetyping]
ret [projection, in MetaRocq.Utils.monad_utils]
Ret [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ret [abbreviation, in MetaRocq.SafeChecker.PCUICTypeChecker]
Retroknowledge [module, in MetaRocq.Common.Environment]
Retroknowledge.compatible [definition, in MetaRocq.Common.Environment]
Retroknowledge.empty [definition, in MetaRocq.Common.Environment]
Retroknowledge.extends [definition, in MetaRocq.Common.Environment]
Retroknowledge.extendsb [definition, in MetaRocq.Common.Environment]
Retroknowledge.extendsT [lemma, in MetaRocq.Common.Environment]
Retroknowledge.extends_r_merge [lemma, in MetaRocq.Common.Environment]
Retroknowledge.extends_merge_idempotent [lemma, in MetaRocq.Common.Environment]
Retroknowledge.extends_l_merge [lemma, in MetaRocq.Common.Environment]
Retroknowledge.extends_trans [instance, in MetaRocq.Common.Environment]
Retroknowledge.extends_refl [instance, in MetaRocq.Common.Environment]
Retroknowledge.extends_spec [lemma, in MetaRocq.Common.Environment]
Retroknowledge.merge [definition, in MetaRocq.Common.Environment]
Retroknowledge.reflect_t [instance, in MetaRocq.Common.Environment]
Retroknowledge.retro_array [projection, in MetaRocq.Common.Environment]
Retroknowledge.retro_string [projection, in MetaRocq.Common.Environment]
Retroknowledge.retro_float64 [projection, in MetaRocq.Common.Environment]
Retroknowledge.retro_int63 [projection, in MetaRocq.Common.Environment]
Retroknowledge.t [record, in MetaRocq.Common.Environment]
rev [definition, in MetaRocq.Utils.MRList]
Reverse_Induction.A [variable, in MetaRocq.Utils.MRList]
Reverse_Induction [section, in MetaRocq.Utils.MRList]
Reverse_Induction.rev_involutive [variable, in MetaRocq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.rev_unit [variable, in MetaRocq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.rev_app_distr [variable, in MetaRocq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.app_assoc [variable, in MetaRocq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.app_nil_r [variable, in MetaRocq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.A [variable, in MetaRocq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction [section, in MetaRocq.PCUIC.Syntax.PCUICInduction]
rev_repeat [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
rev_repeat [lemma, in MetaRocq.Utils.MRList]
rev_case [lemma, in MetaRocq.Utils.MRList]
rev_invol [lemma, in MetaRocq.Utils.MRList]
rev_app [lemma, in MetaRocq.Utils.MRList]
rev_map_spec [lemma, in MetaRocq.Utils.MRList]
rev_mapi [lemma, in MetaRocq.Utils.MRList]
rev_mapi_rec [lemma, in MetaRocq.Utils.MRList]
rev_ind [lemma, in MetaRocq.Utils.MRList]
rev_list_ind [lemma, in MetaRocq.Utils.MRList]
rev_map_app [lemma, in MetaRocq.Utils.MRList]
rev_map_cons [lemma, in MetaRocq.Utils.MRList]
rev_cons [lemma, in MetaRocq.Utils.MRList]
rev_map [definition, in MetaRocq.Utils.MRList]
rev_mapi_length_app [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
rev_inj [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
rev_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
rev_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
rev_list_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
rev_Forall [lemma, in MetaRocq.Utils.All_Forall]
rho [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho [section, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ws_pair [definition, in MetaRocq.PCUIC.PCUICConfluence]
rho_ctx [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_All_All2_fold_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind_terms [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_cofix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_app [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_app [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_lift0 [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_rename_pred [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_proj [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_case [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_elim [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_sind [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_rec [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_ind [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec_rect [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_stuck [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_red [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec [inductive, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_fix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_cofix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_construct [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda' [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context_length [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_length [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_br [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf_gen [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_gen [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_prim_wf_rho_prim [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_map_predicate [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_gen [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf_eq [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope_n.f [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope_n.P [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope_n [section, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope.P [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope [section, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.cf [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.rho_ctx.rho [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.rho_ctx.Γ [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.rho_ctx [section, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.wfΣ [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Rho.Σ [variable, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
right_dlexmod [constructor, in MetaRocq.PCUIC.utils.PCUICUtils]
right_lex [constructor, in MetaRocq.PCUIC.utils.PCUICUtils]
rigid_head [definition, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
rshiftk [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rshiftk_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
rshiftk_S [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
Rtrans [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
rtrans_clos [abbreviation, in MetaRocq.PCUIC.utils.PCUICOnOne]
rtrans_clos_length [lemma, in MetaRocq.PCUIC.PCUICConversion]
rtrans_clos_incl [lemma, in MetaRocq.PCUIC.PCUICReduction]
rt_ctx_t_trans [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_t_refl [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_t_step [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_trans [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_refl [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_step [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_decl_trans [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_decl_refl [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt_ctx_decl_step [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt1n_ctx_trans [constructor, in MetaRocq.PCUIC.PCUICConfluence]
rt1n_ctx_eq [constructor, in MetaRocq.PCUIC.PCUICConfluence]
run_transforms [definition, in MetaRocq.Erasure.Typed.Extraction]
run_transforms_list [definition, in MetaRocq.Erasure.Typed.Extraction]
run_erase_program [definition, in MetaRocq.ErasurePlugin.Erasure]
R_Acc [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_Acc_aux [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_singleton [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_Req_R [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_to_Req [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_positionR [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_aux [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
R_opt [definition, in MetaRocq.Utils.MROption]
R_opt [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
R_stateR [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_stateR [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_positionR2 [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_positionR2 [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_cored2 [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_cored2 [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_positionR [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_positionR [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_cored [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_irrelevance [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_irrelevance [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_Acc [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_Acc [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux [definition, 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) |