| 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) |
O
O [constructor, in MetaRocq.Examples.demo]obpack [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
obseq_lambdabox [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
obseq_compose_assoc [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
occ_betweenP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
odd [definition, in MetaRocq.Examples.demo]
of_global_env_cons [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
of_global_env_cons [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
oi [definition, in MetaRocq.PCUIC.PCUICInductives]
oib [definition, in MetaRocq.PCUIC.PCUICInductives]
Ok [constructor, in MetaRocq.Erasure.Typed.ResultMonad]
old_tag [definition, in MetaRocq.Erasure.EReorderCstrs]
OnConstructor [section, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt [section, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.cdecl [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.cf [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.declc [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.idecl [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.ind [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.mdecl [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.wfΣ [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructorExt.Σ [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.cdecl [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.cf [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.declc [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.idecl [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.ind [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.mdecl [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.wfΣ [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
OnConstructor.Σ [variable, in MetaRocq.PCUIC.PCUICInductiveInversion]
onctx [abbreviation, in MetaRocq.Common.BasicAst]
onctxP [lemma, in MetaRocq.Common.BasicAst]
onctx_eq_ctx_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
onctx_eq_ctx_trans [lemma, in MetaRocq.PCUIC.PCUICEquality]
onctx_eq_ctx_sym [lemma, in MetaRocq.PCUIC.PCUICEquality]
onctx_eq_ctx [lemma, in MetaRocq.PCUIC.PCUICEquality]
onctx_rel [definition, in MetaRocq.PCUIC.Syntax.PCUICInduction]
onctx_k [definition, in MetaRocq.Common.BasicAst]
onctx_k_P [lemma, in MetaRocq.PCUIC.PCUICAst]
onctx_k_shift [lemma, in MetaRocq.PCUIC.PCUICAst]
onctx_k_rev [lemma, in MetaRocq.PCUIC.PCUICAst]
onctx_test [lemma, in MetaRocq.PCUIC.PCUICAst]
onctx_rel [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
onctx_rel_pred1_refl' [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
onctx_rel_pred1_refl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
onctx_fold_context_term [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
onctx_All_fold [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
ondecl [definition, in MetaRocq.Common.BasicAst]
ondeclP [lemma, in MetaRocq.Common.BasicAst]
ondecl_on_free_vars_decl [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
ondecl_map [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ones [definition, in MetaRocq.Examples.demo]
one_inductive_body [record, in MetaRocq.Erasure.Typed.ExAst]
one_inductive_body_eq [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
one_inductive_entry [record, in MetaRocq.PCUIC.PCUICAst]
one_pt_i [definition, in MetaRocq.Examples.demo]
one_list_i [definition, in MetaRocq.Examples.demo]
one_i2 [definition, in MetaRocq.Examples.demo]
one_i [definition, in MetaRocq.Examples.demo]
one_to_one_map_spec [lemma, in MetaRocq.Erasure.EReorderCstrs]
one_to_one_map [definition, in MetaRocq.Erasure.EReorderCstrs]
one_inductive_body [record, in MetaRocq.Erasure.EAst]
one_inductive_entry [record, in MetaRocq.Erasure.EAst]
one_inductive_entry [record, in MetaRocq.Template.Ast]
OnFreeVars [section, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.cf [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pcheck [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pind [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pinfer [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pj [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pprod [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Psort [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.PΓ [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.PΓ_rel [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.wfΣ [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Σ [variable, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
onfvs_app [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnInductives [section, in MetaRocq.Erasure.ErasureFunction]
OnInductives [section, in MetaRocq.PCUIC.PCUICInductives]
OnInductives [section, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.cf [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.cf [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.cf [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.decli [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.decli [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.decli [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.idecl [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.idecl [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.idecl [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.ind [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.ind [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.ind [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.mdecl [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.mdecl [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.mdecl [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.wfΣ [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.wfΣ [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.wfΣ [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.Σ [variable, in MetaRocq.Erasure.ErasureFunction]
OnInductives.Σ [variable, in MetaRocq.PCUIC.PCUICInductives]
OnInductives.Σ [variable, in MetaRocq.PCUIC.PCUICInductives]
only_toplevel [constructor, in MetaRocq.Quotation.ToPCUIC.Init]
only_toplevel [constructor, in MetaRocq.Quotation.ToTemplate.Init]
OnOne_local_2.P [variable, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne_local_2 [section, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2 [inductive, in MetaRocq.Utils.All_Forall]
OnOne2All [inductive, in MetaRocq.Utils.All_Forall]
OnOne2All_All3 [lemma, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
OnOne2All_map2_map_all [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2All_All3 [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_nth_error_impl [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_impl_All_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_nth_error_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_nth_error [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_impl [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_split [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_impl_exist_and_All_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_impl_exist_and_All [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_ind_l [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_exist [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_sym [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_map_all [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_map [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_mapP [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_length2 [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_length [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_app [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_All2_mix_left [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_All_mix_left [lemma, in MetaRocq.Utils.All_Forall]
OnOne2All_sind [definition, in MetaRocq.Utils.All_Forall]
OnOne2All_rec [definition, in MetaRocq.Utils.All_Forall]
OnOne2All_ind [definition, in MetaRocq.Utils.All_Forall]
OnOne2All_rect [definition, in MetaRocq.Utils.All_Forall]
OnOne2All_tl [constructor, in MetaRocq.Utils.All_Forall]
OnOne2All_hd [constructor, in MetaRocq.Utils.All_Forall]
OnOne2All_on_Trel_eq_red_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2All_red_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2All_All2_All2 [lemma, in MetaRocq.Template.TypingWf]
OnOne2All_map2_map_all [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
OnOne2All_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
OnOne2All2i_OnOne2All [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2All2i_OnOne2All [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
OnOne2i [inductive, in MetaRocq.Utils.All_Forall]
OnOne2i_nth_error_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_nth_error [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_impl [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_split [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_impl_exist_and_All_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_impl_exist_and_All [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_ind_l [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_exist [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_sym [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_map [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_mapP [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_length [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_app_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_app [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_All_mix_left [lemma, in MetaRocq.Utils.All_Forall]
OnOne2i_sind [definition, in MetaRocq.Utils.All_Forall]
OnOne2i_rec [definition, in MetaRocq.Utils.All_Forall]
OnOne2i_ind [definition, in MetaRocq.Utils.All_Forall]
OnOne2i_rect [definition, in MetaRocq.Utils.All_Forall]
OnOne2i_tl [constructor, in MetaRocq.Utils.All_Forall]
OnOne2i_hd [constructor, in MetaRocq.Utils.All_Forall]
OnOne2_nth_error [lemma, in MetaRocq.PCUIC.PCUICNormal]
OnOne2_local_env_forget_types [lemma, in MetaRocq.PCUIC.PCUICSR]
OnOne2_All2i_All2i [lemma, in MetaRocq.PCUIC.PCUICSR]
OnOne2_All2_All2 [lemma, in MetaRocq.PCUIC.PCUICSR]
OnOne2_ctx_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
OnOne2_local_env_impl_test [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_test_context_k [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_mapi_context [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_map_context [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_map [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_ondecl_impl [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_impl [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_length [instance, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_sind [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_rec [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_ind [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_rect [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
onone2_localenv_cons_tl [constructor, in MetaRocq.PCUIC.utils.PCUICOnOne]
onone2_localenv_def [constructor, in MetaRocq.PCUIC.utils.PCUICOnOne]
onone2_localenv_cons_abs [constructor, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env [inductive, in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_pred1_ctx_over [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_pars_pred1_ctx_over [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_disj [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_All2_fold [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_exist' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_exist' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_apply_dep [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_local_env_apply [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_sigma [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_apply_All [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_apply [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_prod_assoc [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_prod [lemma, in MetaRocq.PCUIC.PCUICConfluence]
OnOne2_All_All2 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_All_OnOne2 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_All2i_All2 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_local_env_All2_fold [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
OnOne2_map_inv [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_All_All [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_All2_All2 [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_impl_All_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_nth_error_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_nth_error [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_impl [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_split [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_impl_exist_and_All_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_impl_exist_and_All [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_ind_l [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_exist [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_sym [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_map [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_mapP [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_length [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_app_r [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_app [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_All_mix_both [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_All_mix_left [lemma, in MetaRocq.Utils.All_Forall]
OnOne2_sind [definition, in MetaRocq.Utils.All_Forall]
OnOne2_rec [definition, in MetaRocq.Utils.All_Forall]
OnOne2_ind [definition, in MetaRocq.Utils.All_Forall]
OnOne2_rect [definition, in MetaRocq.Utils.All_Forall]
OnOne2_tl [constructor, in MetaRocq.Utils.All_Forall]
OnOne2_hd [constructor, in MetaRocq.Utils.All_Forall]
OnOne2_All2 [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_prod_inv_refl_r [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_prod_inv [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_context_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_on_Trel_eq_red_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_on_Trel_eq_unit [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_red_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
OnOne2_All_All [lemma, in MetaRocq.Template.TypingWf]
OnOne2_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
onPrim [inductive, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimArray [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimFloat [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimInt [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims [inductive, in MetaRocq.Erasure.EPrimitive]
onPrims [section, in MetaRocq.Erasure.EPrimitive]
onPrims [inductive, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsArray [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsArray [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsArrayDep [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsArray_dep [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsFloat [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsFloat [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsFloatDep [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsFloat_dep [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsInt [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsInt [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsIntDep [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsInt_dep [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsString [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsString [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsStringDep [constructor, in MetaRocq.Erasure.EPrimitive]
onPrimsString_dep [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimString [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep [inductive, in MetaRocq.Erasure.EPrimitive]
onPrims_sind [definition, in MetaRocq.Erasure.EPrimitive]
onPrims_rec [definition, in MetaRocq.Erasure.EPrimitive]
onPrims_ind [definition, in MetaRocq.Erasure.EPrimitive]
onPrims_rect [definition, in MetaRocq.Erasure.EPrimitive]
onPrims_map_prop [lemma, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_sind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_rec [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_ind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_rect [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep [inductive, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_sind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_rec [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_ind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_rect [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims.map_onPrims.F [variable, in MetaRocq.Erasure.EPrimitive]
onPrims.map_onPrims.P [variable, in MetaRocq.Erasure.EPrimitive]
onPrims.map_onPrims.R [variable, in MetaRocq.Erasure.EPrimitive]
onPrims.map_onPrims.term' [variable, in MetaRocq.Erasure.EPrimitive]
onPrims.map_onPrims.term [variable, in MetaRocq.Erasure.EPrimitive]
onPrims.map_onPrims [section, in MetaRocq.Erasure.EPrimitive]
onPrim_sind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrim_ind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
OnSubterm [section, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
OnSubterm [section, in MetaRocq.Erasure.EWcbvEvalEtaInd]
OnSubterm [section, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
OnSubterm.etfl [variable, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
OnSubterm.etfl [variable, in MetaRocq.Erasure.EWcbvEvalEtaInd]
OnSubterm.etfl [variable, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
OnUdecl [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
OnUdecl.cf [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
on_free_vars_type [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_branch_type [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_subst0 [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_subst [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_branch_context [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_predicate_context [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_ctx_tip [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_ctx_free_vars_strengthenP [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_rename [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSR]
on_free_vars_ctx_tip [lemma, in MetaRocq.PCUIC.PCUICSR]
on_constructor_closed_indices_inst [lemma, in MetaRocq.PCUIC.PCUICSR]
on_free_vars_closedn [lemma, in MetaRocq.PCUIC.PCUICSR]
on_constructor_wf_arities_pars_args [lemma, in MetaRocq.PCUIC.PCUICSR]
on_constructor_closed_indices [lemma, in MetaRocq.PCUIC.PCUICSR]
on_free_vars_ctx_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICSR]
on_constructor_wf_args [lemma, in MetaRocq.PCUIC.PCUICSR]
on_hyps_sound [lemma, in MetaRocq.Examples.tauto]
on_hyp_sound [lemma, in MetaRocq.Examples.tauto]
on_hyps_size [lemma, in MetaRocq.Examples.tauto]
on_hyp_size [lemma, in MetaRocq.Examples.tauto]
on_hyps [definition, in MetaRocq.Examples.tauto]
on_hyp [definition, in MetaRocq.Examples.tauto]
on_ctx_free_vars_snoc [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
on_constructor_closed [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
on_constructor_closed_arities [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
on_free_vars_ctx_inst_case_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
on_free_vars_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
on_minductive_wf_params_indices_inst_weaken [lemma, in MetaRocq.Erasure.ErasureFunction]
on_minductive_wf_params_weaken [lemma, in MetaRocq.Erasure.ErasureFunction]
on_udecl_on_udecl_prop [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
on_udecl_prop [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
on_universes_true [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
on_subterms_sind [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms_rec [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms_ind [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms_rect [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_force [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_lazy [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_prim [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_cofix [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_fix [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_proj [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_case [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_cstr [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_app [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_letin [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_lambda [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_evar [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_atom [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms [inductive, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_one_decl_test_decl [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_test_impl [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_mapi_context [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_map [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_map_na [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl_impl [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl1 [abbreviation, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_one_decl [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
on_free_vars_ctx_onctx_k [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
on_subterm [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
on_free_vars_ind_predicate_context [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
on_free_vars_decl_lift_impl [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
on_free_vars_decl_lift [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
on_free_vars_decl_eq [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
on_free_vars_any_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
on_free_vars_ctx_fix_context_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
on_ctx_free_vars_fix_context_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
on_free_vars_ctx_inst_case_context_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
on_ctx_free_vars_inst_case_context_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
on_free_vars_ctx_closed_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
on_global_decls_prefix [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
on_global_env_ind [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
on_free_vars_projs [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_mon [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_terms_proper [instance, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_case_predicate_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_subst_k [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_mfix [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ind_params [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_cstr_branch_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ind_predicate_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_k_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_fst [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_decl_trans_on_free_vars_decl [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_subterms_sind [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_rec [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_ind [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_rect [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_force [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_lazy [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_prim [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_cofix [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_fix [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_proj [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_case [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_app [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_letin [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_lambda [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_evar [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_atom [constructor, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms [inductive, in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_sind [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms_rec [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms_ind [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms_rect [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_force [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_lazy [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_prim [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_cofix [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_fix [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_proj [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_case [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_cstr [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_app [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_letin [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_lambda [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_evar [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_atom [constructor, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms [inductive, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_constructor_closed_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_udecl_prop_poly_bounded [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_projections_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_inst_pars_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_inst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_inst_wf_args [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_subst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_constructor_wf_args [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
on_free_vars_ctx_inst_case_context_xpred0 [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_ctx_snoc_def_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_ctx_snoc_ass_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_free_vars_shiftnP_S [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_fvs_letin [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_fvs_lambda [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_fvs_prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
on_minductive_wf_params [lemma, in MetaRocq.PCUIC.PCUICArities]
on_free_vars_ctx_All_fold_over [lemma, in MetaRocq.PCUIC.PCUICAlpha]
on_Some_or_None [definition, in MetaRocq.Utils.MROption]
on_some_or_none [definition, in MetaRocq.Utils.MROption]
on_SomeP [lemma, in MetaRocq.Utils.MROption]
on_Some [definition, in MetaRocq.Utils.MROption]
on_some [definition, in MetaRocq.Utils.MROption]
on_local_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICInduction]
on_ctx_free_vars_fold [definition, in MetaRocq.PCUIC.PCUICContextReduction]
on_ctx_free_vars_cons [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
on_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
on_snd_eq_id_spec [lemma, in MetaRocq.Common.BasicAst]
on_udecl_poly_bounded [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
on_contexts_subst_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_firstn_skipn [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_pred1_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_rename_context [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_fold_context_k [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_context_k [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_refl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_mapi_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_mapi [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app_inv_left [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over_app [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app_ex [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app' [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_impl_ind [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_impl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_length [abbreviation, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_app [abbreviation, in MetaRocq.PCUIC.PCUICParallelReduction]
on_contexts_over [abbreviation, in MetaRocq.PCUIC.PCUICParallelReduction]
on_decls_over [abbreviation, in MetaRocq.PCUIC.PCUICParallelReduction]
on_projections_decl [lemma, in MetaRocq.PCUIC.PCUICInductives]
on_inductive_sort_inst [lemma, in MetaRocq.PCUIC.PCUICInductives]
on_inductive_sort [lemma, in MetaRocq.PCUIC.PCUICInductives]
on_inductive_inst [lemma, in MetaRocq.PCUIC.PCUICInductives]
on_minductive_wf_params_indices_inst [lemma, in MetaRocq.PCUIC.PCUICInductives]
on_minductive_wf_params_indices [lemma, in MetaRocq.PCUIC.PCUICInductives]
on_Trel_trans [instance, in MetaRocq.Utils.MRRelations]
on_Trel_sym [instance, in MetaRocq.Utils.MRRelations]
on_Trel_refl [instance, in MetaRocq.Utils.MRRelations]
on_rel_trans [instance, in MetaRocq.Utils.MRRelations]
on_rel_sym [instance, in MetaRocq.Utils.MRRelations]
on_rel_refl [instance, in MetaRocq.Utils.MRRelations]
on_Trel_eq [abbreviation, in MetaRocq.Utils.MRRelations]
on_Trel [definition, in MetaRocq.Utils.MRRelations]
on_rel [definition, in MetaRocq.Utils.MRRelations]
on_udecl_mono [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
on_global_decls [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
on_ctx_free_vars_xpredT_skipn [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
on_ctx_free_vars_xpredT_snoc [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
on_free_vars_subst_consn [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
on_pi2 [definition, in MetaRocq.Utils.MRProd]
on_snd_eq_spec [lemma, in MetaRocq.Utils.MRProd]
on_snd_on_snd [lemma, in MetaRocq.Utils.MRProd]
on_snd [definition, in MetaRocq.Utils.MRProd]
on_global_inductive_wf_bodies [lemma, in MetaRocq.Template.TypingWf]
on_inductive_wf_params [lemma, in MetaRocq.Template.TypingWf]
on_global_inductive_wf_params [lemma, in MetaRocq.Template.TypingWf]
on_global_decls_extends_not_fresh [lemma, in MetaRocq.Template.TypingWf]
on_global_env_impl [lemma, in MetaRocq.Template.TypingWf]
on_global_decl_impl [lemma, in MetaRocq.Template.TypingWf]
on_free_vars_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICClassification]
on_ctx_universes [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
on_decl_universes [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
on_universes_subst [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
on_universes_lift [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
on_universes [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
on_inl [definition, in MetaRocq.Common.uGraph]
on_fst [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
on_ctx_free_vars_xpredT [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_prod_inv [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_prod [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctxs [definition, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_ctx_free_vars_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_decls [definition, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_inst_case_context_nil [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_rename_S [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_all_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_def [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_ass [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_fix_context_weak [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_fix_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_inst_case_context_weak [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_inst_case_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snocS [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc_def [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc_ass [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_closedP_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_closedP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_any_xpredT [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_All_fold [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context_xpredT [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_smash [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_lift_context0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_lift_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_vdef [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_vass [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_inst_case_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_fix_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_extend [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_xpredT [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_tip [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_concat [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_unfold_cofix [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_cofix_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_unfold_fix [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_fix_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_to_extended_list [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_map2_cstr_args [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_map [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms_inds [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_expand_lets_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_extended_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_implP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_k [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_all_term [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_all_term [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift0_above [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_proper_pointwise [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst1 [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst_gen [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_proper_pointwise [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_proper_pointwise [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ext [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_global_decl_wf [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
on_global_env_impl [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
on_pair [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
on_snd_eq_id_spec [lemma, in MetaRocq.Erasure.ELiftSubst]
on_declared_projection [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_constructor [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_inductive [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_minductive [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_constant [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
open_decl_proj [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
open_decl [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
open_context [abbreviation, in MetaRocq.PCUIC.PCUICContextConversion]
open_term [abbreviation, in MetaRocq.PCUIC.PCUICConfluence]
optimize [abbreviation, in MetaRocq.Erasure.EReorderCstrs]
optimize [definition, in MetaRocq.Erasure.EInlineProjections]
optimize [section, in MetaRocq.Erasure.EInlineProjections]
Optimize [library]
OptimizeCorrectness [library]
optimized_abstract_env_impl [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_prop [instance, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_struct [instance, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
OptimizePropDiscr [library]
optimize_prop_discr [projection, in MetaRocq.Erasure.Typed.Extraction]
optimize_correct [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
optimize_extends_env [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded_decl_fix [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded_fix [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded_decl [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_expanded [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_correct [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_cunfold_cofix [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_cunfold_fix [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_cofix_subst [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_fix_subst [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_iota_red [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_substl [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_csubst [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_mkApps [lemma, in MetaRocq.Erasure.EReorderCstrs]
optimize_program_expanded [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_program_wf [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_program [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_env_wf [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_env_expanded [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_env_eq [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_extends_env [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_wellformed [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_wellformed_irrel [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_wellformed_term [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_expanded_decl_irrel [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_expanded_decl [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_expanded_irrel [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_expanded [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_correct [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_env' [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_env [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_decl [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_constant_decl [definition, in MetaRocq.Erasure.EInlineProjections]
optimize_cunfold_cofix [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_cunfold_fix [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_cofix_subst [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_fix_subst [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_iota_red [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_substl [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_csubst [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize_mkApps [lemma, in MetaRocq.Erasure.EInlineProjections]
optimize.Σ [variable, in MetaRocq.Erasure.EInlineProjections]
optim_pop [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
optional_self_transformation_ext [instance, in MetaRocq.ErasurePlugin.ETransform]
optional_self_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
optional_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
optional_unsafe_transforms [definition, in MetaRocq.ErasurePlugin.Erasure]
option_extends_trans [instance, in MetaRocq.Utils.MROption]
option_extends_refl [instance, in MetaRocq.Utils.MROption]
option_extends_spec [lemma, in MetaRocq.Utils.MROption]
option_extendsT [lemma, in MetaRocq.Utils.MROption]
option_extendsb [definition, in MetaRocq.Utils.MROption]
option_extends_sind [definition, in MetaRocq.Utils.MROption]
option_extends_ind [definition, in MetaRocq.Utils.MROption]
option_ext_non [constructor, in MetaRocq.Utils.MROption]
option_ext_keep [constructor, in MetaRocq.Utils.MROption]
option_ext_fill [constructor, in MetaRocq.Utils.MROption]
option_extends [inductive, in MetaRocq.Utils.MROption]
option_map_Some [lemma, in MetaRocq.Utils.MROption]
option_map_id [lemma, in MetaRocq.Utils.MROption]
option_map_proper [instance, in MetaRocq.Utils.MROption]
option_map_ext [lemma, in MetaRocq.Utils.MROption]
option_map_two [lemma, in MetaRocq.Utils.MROption]
option_default_ext [lemma, in MetaRocq.Utils.MROption]
option_default [definition, in MetaRocq.Utils.MROption]
option_get [definition, in MetaRocq.Utils.MROption]
option_monad_exc [instance, in MetaRocq.Utils.monad_utils]
option_monad [instance, in MetaRocq.Utils.monad_utils]
option_map_decl_type_map_decl [lemma, in MetaRocq.Common.BasicAst]
option_map_decl_body_map_decl [lemma, in MetaRocq.Common.BasicAst]
option_instance_sind [definition, in MetaRocq.Template.TemplateMonad.Common]
option_instance_rec [definition, in MetaRocq.Template.TemplateMonad.Common]
option_instance_ind [definition, in MetaRocq.Template.TemplateMonad.Common]
option_instance_rect [definition, in MetaRocq.Template.TemplateMonad.Common]
option_instance [inductive, in MetaRocq.Template.TemplateMonad.Common]
option_is_none [definition, in MetaRocq.Erasure.Extract]
option_edge_of_level [definition, in MetaRocq.Common.uGraph]
option_UIP [instance, in MetaRocq.PCUIC.PCUICWcbvEval]
opt_variance [inductive, in MetaRocq.Common.Universes]
opt_wcbv_flags [definition, in MetaRocq.Erasure.EWcbvEval]
opt_bool_to_bool [definition, in MetaRocq.Template.Checker]
Or [constructor, in MetaRocq.Examples.tauto]
orPL [lemma, in MetaRocq.Utils.MRPred]
orPL [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
orPR [lemma, in MetaRocq.Utils.MRPred]
orPR [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
orP_Proper [instance, in MetaRocq.Utils.MRPred]
orP_Proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
OT_byte.eq_dec [definition, in MetaRocq.Utils.bytestring]
OT_byte.compare [definition, in MetaRocq.Utils.bytestring]
OT_byte.lt_not_eq [lemma, in MetaRocq.Utils.bytestring]
OT_byte.lt_trans [lemma, in MetaRocq.Utils.bytestring]
OT_byte.eq_trans [lemma, in MetaRocq.Utils.bytestring]
OT_byte.eq_sym [lemma, in MetaRocq.Utils.bytestring]
OT_byte.eq_refl [lemma, in MetaRocq.Utils.bytestring]
OT_byte.lt [definition, in MetaRocq.Utils.bytestring]
OT_byte.eq [definition, in MetaRocq.Utils.bytestring]
OT_byte.t [definition, in MetaRocq.Utils.bytestring]
OT_byte [module, in MetaRocq.Utils.bytestring]
overridden_masks [projection, in MetaRocq.ErasurePlugin.ETransform]
| 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) |