| 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 (definition)
occ_betweenP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]odd [in MetaRocq.Examples.demo]
oi [in MetaRocq.PCUIC.PCUICInductives]
oib [in MetaRocq.PCUIC.PCUICInductives]
old_tag [in MetaRocq.Erasure.EReorderCstrs]
onctx_rel [in MetaRocq.PCUIC.Syntax.PCUICInduction]
onctx_k [in MetaRocq.Common.BasicAst]
onctx_rel [in MetaRocq.PCUIC.Syntax.PCUICDepth]
ondecl [in MetaRocq.Common.BasicAst]
ones [in MetaRocq.Examples.demo]
one_pt_i [in MetaRocq.Examples.demo]
one_list_i [in MetaRocq.Examples.demo]
one_i2 [in MetaRocq.Examples.demo]
one_i [in MetaRocq.Examples.demo]
one_to_one_map [in MetaRocq.Erasure.EReorderCstrs]
OnOne2All_sind [in MetaRocq.Utils.All_Forall]
OnOne2All_rec [in MetaRocq.Utils.All_Forall]
OnOne2All_ind [in MetaRocq.Utils.All_Forall]
OnOne2All_rect [in MetaRocq.Utils.All_Forall]
OnOne2i_sind [in MetaRocq.Utils.All_Forall]
OnOne2i_rec [in MetaRocq.Utils.All_Forall]
OnOne2i_ind [in MetaRocq.Utils.All_Forall]
OnOne2i_rect [in MetaRocq.Utils.All_Forall]
OnOne2_local_env_sind [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_rec [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_ind [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_rect [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_sind [in MetaRocq.Utils.All_Forall]
OnOne2_rec [in MetaRocq.Utils.All_Forall]
OnOne2_ind [in MetaRocq.Utils.All_Forall]
OnOne2_rect [in MetaRocq.Utils.All_Forall]
onPrims_sind [in MetaRocq.Erasure.EPrimitive]
onPrims_rec [in MetaRocq.Erasure.EPrimitive]
onPrims_ind [in MetaRocq.Erasure.EPrimitive]
onPrims_rect [in MetaRocq.Erasure.EPrimitive]
onPrims_dep_sind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_rec [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_ind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_dep_rect [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_sind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_rec [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_ind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrims_rect [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrim_sind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrim_ind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
on_hyps [in MetaRocq.Examples.tauto]
on_hyp [in MetaRocq.Examples.tauto]
on_udecl_prop [in MetaRocq.PCUIC.PCUICWeakeningEnv]
on_subterms_sind [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms_rec [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms_ind [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_subterms_rect [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_one_decl [in MetaRocq.PCUIC.utils.PCUICOnOne]
on_subterm [in MetaRocq.SafeChecker.PCUICSafeRetyping]
on_free_vars_mfix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_fst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
on_subterms_sind [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_rec [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_ind [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_rect [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_subterms_sind [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms_rec [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms_ind [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_subterms_rect [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_Some_or_None [in MetaRocq.Utils.MROption]
on_some_or_none [in MetaRocq.Utils.MROption]
on_Some [in MetaRocq.Utils.MROption]
on_some [in MetaRocq.Utils.MROption]
on_local_decl [in MetaRocq.PCUIC.Syntax.PCUICInduction]
on_ctx_free_vars_fold [in MetaRocq.PCUIC.PCUICContextReduction]
on_Trel [in MetaRocq.Utils.MRRelations]
on_rel [in MetaRocq.Utils.MRRelations]
on_global_decls [in MetaRocq.SafeChecker.PCUICWfEnv]
on_pi2 [in MetaRocq.Utils.MRProd]
on_snd [in MetaRocq.Utils.MRProd]
on_ctx_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
on_decl_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
on_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
on_inl [in MetaRocq.Common.uGraph]
on_fst [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
on_free_vars_ctxs [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_decls [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_k [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
on_pair [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
open_decl_proj [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
open_decl [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
optimize [in MetaRocq.Erasure.EInlineProjections]
optimized_abstract_env_impl [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
optimize_program_expanded [in MetaRocq.Erasure.EInlineProjections]
optimize_program_wf [in MetaRocq.Erasure.EInlineProjections]
optimize_program [in MetaRocq.Erasure.EInlineProjections]
optimize_env' [in MetaRocq.Erasure.EInlineProjections]
optimize_env [in MetaRocq.Erasure.EInlineProjections]
optimize_decl [in MetaRocq.Erasure.EInlineProjections]
optimize_constant_decl [in MetaRocq.Erasure.EInlineProjections]
optim_pop [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
optional_self_transform [in MetaRocq.ErasurePlugin.ETransform]
optional_transform [in MetaRocq.ErasurePlugin.ETransform]
optional_unsafe_transforms [in MetaRocq.ErasurePlugin.Erasure]
option_extendsb [in MetaRocq.Utils.MROption]
option_extends_sind [in MetaRocq.Utils.MROption]
option_extends_ind [in MetaRocq.Utils.MROption]
option_default [in MetaRocq.Utils.MROption]
option_get [in MetaRocq.Utils.MROption]
option_instance_sind [in MetaRocq.Template.TemplateMonad.Common]
option_instance_rec [in MetaRocq.Template.TemplateMonad.Common]
option_instance_ind [in MetaRocq.Template.TemplateMonad.Common]
option_instance_rect [in MetaRocq.Template.TemplateMonad.Common]
option_is_none [in MetaRocq.Erasure.Extract]
option_edge_of_level [in MetaRocq.Common.uGraph]
opt_wcbv_flags [in MetaRocq.Erasure.EWcbvEval]
opt_bool_to_bool [in MetaRocq.Template.Checker]
OT_byte.eq_dec [in MetaRocq.Utils.bytestring]
OT_byte.compare [in MetaRocq.Utils.bytestring]
OT_byte.lt [in MetaRocq.Utils.bytestring]
OT_byte.eq [in MetaRocq.Utils.bytestring]
OT_byte.t [in MetaRocq.Utils.bytestring]
| 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) |