| 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) |
P
P [module, in MetaRocq.Erasure.Typed.Erasure]P [module, in MetaRocq.Erasure.Typed.ErasureCorrectness]
P [module, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
pack [record, in MetaRocq.SafeChecker.PCUICSafeConversion]
packed_constructor [record, in MetaRocq.Template.Lib]
packed_inductive [record, in MetaRocq.Template.Lib]
Pand [projection, in MetaRocq.Examples.tauto]
ParallelReduction [section, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx_over _ _ [notation, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx [notation, in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelReduction.Σ [variable, in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelSubstitution [section, in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelSubstitution.cf [variable, in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelSubstitution.Σ [variable, in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelWeakening [section, in MetaRocq.PCUIC.PCUICParallelReduction]
ParallelWeakening.cf [variable, in MetaRocq.PCUIC.PCUICParallelReduction]
ParameterEntry [constructor, in MetaRocq.PCUIC.PCUICAst]
ParameterEntry [constructor, in MetaRocq.Erasure.EAst]
ParameterEntry [constructor, in MetaRocq.Template.Ast]
parameter_entry_universes [projection, in MetaRocq.PCUIC.PCUICAst]
parameter_entry_type [projection, in MetaRocq.PCUIC.PCUICAst]
parameter_entry [record, in MetaRocq.PCUIC.PCUICAst]
parameter_entry [record, in MetaRocq.Erasure.EAst]
parameter_entry_universes [projection, in MetaRocq.Template.Ast]
parameter_entry_type [projection, in MetaRocq.Template.Ast]
parameter_entry [record, in MetaRocq.Template.Ast]
params_subslet [lemma, in MetaRocq.PCUIC.PCUICNormal]
param_mask [projection, in MetaRocq.Erasure.Typed.Optimize]
param_original [library]
param_binary [library]
param_cheap_packed [library]
param_generous_unpacked [library]
param_generous_packed [library]
parens [definition, in MetaRocq.Utils.MRString]
PathOf_proper_weight [lemma, in MetaRocq.Common.uGraph]
PathOf_proper [lemma, in MetaRocq.Common.uGraph]
pb_of_dec [definition, in MetaRocq.Quotation.CommonUtils]
pclengths [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
pcontext [projection, in MetaRocq.PCUIC.PCUICAst]
pcontext [projection, in MetaRocq.Template.Ast]
PCUICAlpha [library]
PCUICArities [library]
PCUICAst [library]
PCUICAstUtils [library]
PCUICCanonicity [library]
PCUICCases [library]
PCUICCasesContexts [library]
PCUICCasesHelper [library]
PCUICClassification [library]
PCUICClosed [library]
PCUICClosedConv [library]
PCUICClosedTyp [library]
PCUICConfluence [library]
PCUICConsistency [library]
PCUICContextConversion [library]
PCUICContextConversionTyp [library]
PCUICContextReduction [library]
PCUICContexts [library]
PCUICContextSubst [library]
PCUICConvCumInversion [library]
PCUICConversion [module, in MetaRocq.PCUIC.PCUICAst]
PCUICConversion [library]
PCUICConversionParAlgo [module, in MetaRocq.PCUIC.PCUICCumulativity]
PCUICConversionParAlgo.cumul_gen [definition, in MetaRocq.PCUIC.PCUICCumulativity]
PCUICConversionParSpec [module, in MetaRocq.PCUIC.PCUICCumulativitySpec]
PCUICConversionParSpec.cumul_gen [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
PCUICCSubst [library]
PCUICCumulativity [library]
PCUICCumulativitySpec [library]
PCUICCumulProp [library]
PCUICDeclarationTyping [module, in MetaRocq.PCUIC.PCUICTyping]
PCUICDepth [library]
PCUICElimination [library]
PCUICenv [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
PCUICEnv [section, in MetaRocq.ErasurePlugin.ETransform]
PCUICEnvironment [module, in MetaRocq.PCUIC.PCUICAst]
PCUICEnvironmentDecide [module, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.constant_body_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.constructor_body_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.context_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.global_decl_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.mutual_inductive_body_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.one_inductive_body_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentDecide.projection_body_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvironmentReflect [module, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICEnvTyping [module, in MetaRocq.PCUIC.PCUICAst]
PCUICEquality [library]
PCUICEqualityDec [library]
PCUICErase [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
PCUICErrors [library]
PCUICEtaExpand [library]
PCUICExpandLets [library]
PCUICExpandLetsCorrectness [library]
PCUICFirstorder [library]
PCUICGeneration [library]
PCUICGlobalEnv [library]
PCUICGlobalMaps [module, in MetaRocq.PCUIC.PCUICAst]
PCUICGuardCondition [library]
PCUICInduction [library]
PCUICInductiveInversion [library]
PCUICInductives [library]
PCUICInstConv [library]
PCUICInstDef [library]
PCUICInstTyp [library]
PCUICInv [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
PCUICInversion [library]
PCUICLiftSubst [library]
PCUICLoader [library]
PCUICLookup [module, in MetaRocq.PCUIC.PCUICAst]
PCUICMonadAst [library]
PCUICNamelessConv [library]
PCUICNamelessDef [library]
PCUICNamelessTyp [library]
PCUICNormal [library]
PCUICNormalization [library]
PCUICOnFreeVars [library]
PCUICOnFreeVarsConv [library]
PCUICOnOne [library]
PCUICParallelReduction [library]
PCUICParallelReductionConfluence [library]
PCUICPosition [library]
PCUICPretty [library]
PCUICPrimitive [library]
PCUICPrincipality [library]
PCUICProgram [library]
PCUICProgress [library]
PCUICProof [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
PCUICRedTypeIrrelevance [library]
PCUICReduction [library]
PCUICReflect [library]
PCUICRenameConv [library]
PCUICRenameDef [library]
PCUICRenameTyp [library]
PCUICRetypingEnvIrrelevance [library]
PCUICSafeChecker [library]
PCUICSafeConversion [library]
PCUICSafeLemmata [library]
PCUICSafeReduce [library]
PCUICSafeRetyping [library]
PCUICSigmaCalculus [library]
PCUICSize [library]
PCUICSN [library]
PCUICSpine [library]
PCUICSR [library]
PCUICSubstitution [library]
PCUICTactics [library]
PCUICTelescopes [library]
PCUICTemplateMonad [library]
PCUICTerm [module, in MetaRocq.PCUIC.PCUICAst]
PCUICTermDecide [module, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICTermDecide.term_eq_dec [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
PCUICTermUtils [module, in MetaRocq.PCUIC.PCUICAst]
PCUICTermUtils.destArity [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTermUtils.inds [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.closedn [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.lift [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.mkApps [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.noccur_between [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.subst [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.subst_instance_constr [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.term [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tInd [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tLambda [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tLetIn [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tProd [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tProj [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tRel [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tSort [definition, in MetaRocq.PCUIC.PCUICAst]
PCUICToTemplate [library]
PCUICToTemplateCorrectness [library]
PCUICTransform [library]
PCUICTypeChecker [library]
PCUICTypedAst [library]
PCUICTyping [library]
PCUICTypingDef [module, in MetaRocq.PCUIC.PCUICTyping]
PCUICTypingDef.typing [definition, in MetaRocq.PCUIC.PCUICTyping]
PCUICUnivLevels [library]
PCUICUnivSubst [library]
PCUICUnivSubstitutionConv [library]
PCUICUnivSubstitutionTyp [library]
PCUICUtils [library]
PCUICValidity [library]
PCUICViews [library]
PCUICWcbvEval [library]
PCUICWeakeningConfig [library]
PCUICWeakeningConfigConv [library]
PCUICWeakeningConfigSN [library]
PCUICWeakeningConfigTyp [library]
PCUICWeakeningConv [library]
PCUICWeakeningEnv [library]
PCUICWeakeningEnvConv [library]
PCUICWeakeningEnvSN [library]
PCUICWeakeningEnvTyp [library]
PCUICWeakeningTyp [library]
PCUICWellScopedCumulativity [library]
PCUICWfCases [library]
PCUICWfEnv [library]
PCUICWfEnvImpl [library]
PCUICWfReduction [library]
PCUICWfUniverses [library]
PCUICWtCumulativity [library]
pcuic_args [projection, in MetaRocq.Erasure.Typed.Extraction]
pcuic_program [definition, in MetaRocq.PCUIC.PCUICProgram]
pcuic_canonicity [lemma, in MetaRocq.PCUIC.PCUICCanonicity]
pcuic_quotation_red_strategy [projection, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
pcuic_quotation_red_strategy [constructor, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
pcuic_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
pcuic_function_value [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pcuic_eval_function [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pcuic_lookup_inductive_pars [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pcuic_consistent [lemma, in MetaRocq.PCUIC.PCUICConsistency]
pcuic_expand_lets_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
pcuic_to_template [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
pcuic_expand_lets_transform [definition, in MetaRocq.TemplatePCUIC.PCUICTransform]
pc_body [projection, in MetaRocq.Template.Lib]
pc_idx [projection, in MetaRocq.Template.Lib]
pc_pi [projection, in MetaRocq.Template.Lib]
PEnv [module, in MetaRocq.Erasure.Typed.Extraction]
PEnv [module, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
permute_lift0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
permute_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
permute_lift0 [lemma, in MetaRocq.Template.LiftSubst]
permute_lift [lemma, in MetaRocq.Template.LiftSubst]
permute_lift0 [lemma, in MetaRocq.Erasure.ELiftSubst]
permute_lift [lemma, in MetaRocq.Erasure.ELiftSubst]
Pfalse [projection, in MetaRocq.Examples.tauto]
pick_hyp_def [lemma, in MetaRocq.Examples.tauto]
pick_hyp [definition, in MetaRocq.Examples.tauto]
Pimpl [projection, in MetaRocq.Examples.tauto]
pipeline_theorem.v_t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Σ_v [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.t_t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Σ_t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Heval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.fo [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.typing [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Normalisation [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.args [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.u [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.i [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.v [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.axfree [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.expt [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.expΣ [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.HΣ [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem.Σ [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_theorem [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.v_t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Σ_v [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.t_t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Σ_t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Heval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.v [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Normalisation [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.typing [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.expt [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.expΣ [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.HΣ [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.T [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.t [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond.Σ [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pipeline_cond [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pi_block [definition, in MetaRocq.Template.Lib]
pi_ctors [definition, in MetaRocq.Template.Lib]
pi_mbody [projection, in MetaRocq.Template.Lib]
pi_body [projection, in MetaRocq.Template.Lib]
pi_ind [projection, in MetaRocq.Template.Lib]
plengths [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
plengths [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
plookup_env_extends [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
plookup_env_Some_not_fresh [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
plookup_env_lookup_env [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
plookup_env [definition, in MetaRocq.PCUIC.PCUICFirstorder]
Plugin [section, in MetaRocq.Examples.tauto]
plus_minus' [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
pointwise_subrelation2 [instance, in MetaRocq.Utils.MRPrelude]
pointwise_subrelation [instance, in MetaRocq.Utils.MRPrelude]
PolymorphicInstances [module, in MetaRocq.Quotation.ToPCUIC.Init]
PolymorphicInstances [module, in MetaRocq.Quotation.ToTemplate.Init]
PolymorphicInstances.quote_relax_universe [instance, in MetaRocq.Quotation.ToPCUIC.Init]
PolymorphicInstances.quote_relax_universe [instance, in MetaRocq.Quotation.ToTemplate.Init]
polymorphic_instance [definition, in MetaRocq.Common.Universes]
Polymorphic_entry [constructor, in MetaRocq.Common.Universes]
Polymorphic_ctx [constructor, in MetaRocq.Common.Universes]
polymorphic_constraints [definition, in MetaRocq.Template.Checker]
Por [projection, in MetaRocq.Examples.tauto]
pos [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
poscat_valid [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
poscat_atpos [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
position [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_stack_pos_xpos [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_xposition_inv [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_context_position_inv [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_poscat_nonil [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_trans [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_poscat [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_root [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_deep [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_app_lr [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
positive [inductive, in MetaRocq.Utils.canonicaltries.String2pos]
positive_cstr_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_arg_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_smash_middle [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_closed_indices' [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_args [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_args_subst_arities [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_arg_subst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_arg_subst_instance [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_sind [definition, in MetaRocq.Utils.canonicaltries.String2pos]
positive_rec [definition, in MetaRocq.Utils.canonicaltries.String2pos]
positive_ind [definition, in MetaRocq.Utils.canonicaltries.String2pos]
positive_rect [definition, in MetaRocq.Utils.canonicaltries.String2pos]
posR [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
posR_trans [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
posR_Acc [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
post_dearging_checks [definition, in MetaRocq.ErasurePlugin.ETransform]
pos_of_string [definition, in MetaRocq.Utils.canonicaltries.String2pos]
pparams [projection, in MetaRocq.PCUIC.PCUICAst]
pparams [projection, in MetaRocq.Template.Ast]
pps1 [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
pps2 [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
Pr [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
pr [definition, in MetaRocq.Erasure.EPretty]
prec [definition, in MetaRocq.Common.BasicAst]
precompose_subst_instance_global__2 [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance_global__1 [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance_global [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance__2 [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance__1 [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precond [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
precond2 [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
predA [definition, in MetaRocq.Utils.MRPred]
predA [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
predicate [record, in MetaRocq.PCUIC.PCUICAst]
predicate [record, in MetaRocq.Template.Ast]
predicate_hole_pars [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
predicate_hole_context [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
predicate_hole [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
predicate_size [definition, in MetaRocq.Examples.tauto]
predicate_size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
predicate_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
predicate_depth [abbreviation, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
predicate_eq_dec [instance, in MetaRocq.Template.Ast]
PredRed [section, in MetaRocq.PCUIC.PCUICConfluence]
PredRed.cf [variable, in MetaRocq.PCUIC.PCUICConfluence]
PredRed.wfΣ [variable, in MetaRocq.PCUIC.PCUICConfluence]
PredRed.Σ [variable, in MetaRocq.PCUIC.PCUICConfluence]
pred_hole_return [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
pred_hole_params [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
pred_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred_rel_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred_atom_inst [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_atom_refl [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_prod [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_cofix_congr [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_fix_congr [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_proj_congr [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_case [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_letin [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_app [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_abs [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_proj [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_const [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_delta [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_cofix_proj [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_cofix_case [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_fix [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_iota [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_rel_refl [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_rel_def_unfold [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_zeta [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_beta [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_atom [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
pred_subst_rho_fix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_subst_rho_cofix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_mkApps [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_snd_nth [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_atom_mkApps [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_of_simpl_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
pred1 [inductive, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rel_alpha_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_upto_names_gen [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel_alpha_red1_rel_alpha [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel_alpha [definition, in MetaRocq.PCUIC.PCUICConfluence]
pred1_red' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_red_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel_confluent [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel [definition, in MetaRocq.PCUIC.PCUICConfluence]
pred1_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
pred1_on_free_vars_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_red_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_pred1_r' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_pred1_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_red_r_gen' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_red_r_gen [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_pred1_inv [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_over_assumption_context [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_assumption_context [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_pred1 [lemma, in MetaRocq.PCUIC.PCUICConfluence]
pred1_subst_context [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_up [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_Upn [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_vdef_Up [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_Up [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_ext [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_pred1_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx_over [abbreviation, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx [abbreviation, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx_over_refl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_refl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx_refl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_refl_gen [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_pred1_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ind_all_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_sind [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rec [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ind [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rect [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_diamond [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_ctx_over_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_ctx_over_refl_gen [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_expand_lets [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_ext [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_subst_consn [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_rho_fix_context_2 [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_fix_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_mfix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_over_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_gen [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_mfix_ind [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tCoFix_refl_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tCoFix_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tFix_refl_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tFix_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tConst_axiom [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tRel [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tInd [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_refl_tConstruct [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tConstruct [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Pred1_inversion [section, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Prelim [library]
preserves_expansion_env [definition, in MetaRocq.ErasurePlugin.ETransform]
preserves_expansion [definition, in MetaRocq.ErasurePlugin.ETransform]
pres_let_bodies_ctx_refl [lemma, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies_trans [instance, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies_refl [instance, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies [definition, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
pres_let_bodies_assumption_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
pres_inductives_lookup [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
pres_bodies_rename' [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies_inst_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Pretty [library]
pretty_string_of_branch [definition, in MetaRocq.PCUIC.PCUICAst]
pretty_string_of_branch [definition, in MetaRocq.Template.Ast]
preturn [projection, in MetaRocq.PCUIC.PCUICAst]
preturn [projection, in MetaRocq.Template.Ast]
pre_case_predicate_context_gen_eq [lemma, in MetaRocq.PCUIC.PCUICElimination]
pre_type_mkApps_arity [lemma, in MetaRocq.PCUIC.PCUICSpine]
Pre_glob [definition, in MetaRocq.Erasure.EGenericGlobalMap]
Pre_decl [definition, in MetaRocq.Erasure.EGenericGlobalMap]
pre_case_branch_context_eq [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
pre_case_branch_context_length_args [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
pre_case_branch_context [definition, in MetaRocq.PCUIC.PCUICCasesContexts]
Pre_glob [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
Pre_glob [definition, in MetaRocq.Erasure.EGenericMapEnv]
Pre_decl [definition, in MetaRocq.Erasure.EGenericMapEnv]
Pre_glob [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
pre_remove_match_on_box_typed_fresh [lemma, in MetaRocq.ErasurePlugin.ETransform]
pre_remove_match_on_box_typed [definition, in MetaRocq.ErasurePlugin.ETransform]
pre_erasure_pipeline_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
pre_erasure_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
Pre_glob [lemma, in MetaRocq.Erasure.EInlineProjections]
pre_case_branch_context_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
pre_case_predicate_context_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
pre_case_predicate_context_gen [definition, in MetaRocq.Template.Ast]
pre_case_branch_context_gen_length [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
pre_case_predicate_context_gen_indpred_ctx [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
primArray [constructor, in MetaRocq.Common.Primitive]
primArrayModel [constructor, in MetaRocq.Erasure.EPrimitive]
primArrayModel [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
primArrayValue [constructor, in MetaRocq.Erasure.EWcbvEval]
primArrayValue [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
PrimArray_val [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
PrimArray_def [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
PrimArray_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
PrimDeps [section, in MetaRocq.Erasure.EAstUtils]
PrimDeps.deps [variable, in MetaRocq.Erasure.EAstUtils]
prime_tsl_ident [instance, in MetaRocq.Examples.add_constructor]
primFloat [constructor, in MetaRocq.Common.Primitive]
primFloatModel [constructor, in MetaRocq.Erasure.EPrimitive]
primFloatModel [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
primFloatValue [constructor, in MetaRocq.Erasure.EWcbvEval]
primFloatValue [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
PrimIn [section, in MetaRocq.Erasure.EPrimitive]
primInt [constructor, in MetaRocq.Common.Primitive]
primIntModel [constructor, in MetaRocq.Erasure.EPrimitive]
primIntModel [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
primIntValue [constructor, in MetaRocq.Erasure.EWcbvEval]
primIntValue [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
PrimIn.term [variable, in MetaRocq.Erasure.EPrimitive]
Primitive [library]
PrimitiveSize [section, in MetaRocq.PCUIC.PCUICTyping]
PrimitiveSize.cf [variable, in MetaRocq.PCUIC.PCUICTyping]
PrimitiveSize.typing [variable, in MetaRocq.PCUIC.PCUICTyping]
PrimitiveSize.typing_size [variable, in MetaRocq.PCUIC.PCUICTyping]
primitive_typing_hyps_size [definition, in MetaRocq.PCUIC.PCUICTyping]
primitive_typing_hyps [inductive, in MetaRocq.PCUIC.PCUICTyping]
primitive_value [inductive, in MetaRocq.Erasure.EWcbvEval]
primitive_invariants_axiom [lemma, in MetaRocq.Erasure.EArities]
primitive_value [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
PrimModel [section, in MetaRocq.Erasure.EPrimitive]
PrimModel.term [variable, in MetaRocq.Erasure.EPrimitive]
PrimOps [section, in MetaRocq.Erasure.EPrimitive]
PrimOps.term [variable, in MetaRocq.Erasure.EPrimitive]
PrimOps.term' [variable, in MetaRocq.Erasure.EPrimitive]
primProp [inductive, in MetaRocq.Erasure.EPrimitive]
primPropArray [constructor, in MetaRocq.Erasure.EPrimitive]
primPropFloat [constructor, in MetaRocq.Erasure.EPrimitive]
primPropInt [constructor, in MetaRocq.Erasure.EPrimitive]
primPropString [constructor, in MetaRocq.Erasure.EPrimitive]
primProp_mapu_id [lemma, in MetaRocq.PCUIC.PCUICAst]
primProp_map_inv [lemma, in MetaRocq.PCUIC.PCUICAst]
primProp_map [lemma, in MetaRocq.PCUIC.PCUICAst]
primProp_test_prim [lemma, in MetaRocq.PCUIC.PCUICAst]
primProp_map_id [lemma, in MetaRocq.PCUIC.PCUICAst]
primProp_map_eq [lemma, in MetaRocq.PCUIC.PCUICAst]
primProp_map [lemma, in MetaRocq.Erasure.EPrimitive]
primProp_impl [lemma, in MetaRocq.Erasure.EPrimitive]
primProp_conj [lemma, in MetaRocq.Erasure.EPrimitive]
primProp_impl_test_prim [lemma, in MetaRocq.Erasure.EPrimitive]
primProp_sind [definition, in MetaRocq.Erasure.EPrimitive]
primProp_rec [definition, in MetaRocq.Erasure.EPrimitive]
primProp_ind [definition, in MetaRocq.Erasure.EPrimitive]
primProp_rect [definition, in MetaRocq.Erasure.EPrimitive]
primString [constructor, in MetaRocq.Common.Primitive]
primStringModel [constructor, in MetaRocq.Erasure.EPrimitive]
primStringModel [constructor, in MetaRocq.PCUIC.utils.PCUICPrimitive]
primStringValue [constructor, in MetaRocq.Erasure.EWcbvEval]
primStringValue [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
primtheory [section, in MetaRocq.Erasure.EPrimitive]
primtheory [section, in MetaRocq.Erasure.EPrimitive]
primtheory.f [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.g [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.p [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.p [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.term [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.term [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.term' [variable, in MetaRocq.Erasure.EPrimitive]
primtheory.term'' [variable, in MetaRocq.Erasure.EPrimitive]
prim_type [definition, in MetaRocq.PCUIC.PCUICTyping]
prim_array_hyps [constructor, in MetaRocq.PCUIC.PCUICTyping]
prim_string_hyps [constructor, in MetaRocq.PCUIC.PCUICTyping]
prim_float_hyps [constructor, in MetaRocq.PCUIC.PCUICTyping]
prim_int_hyps [constructor, in MetaRocq.PCUIC.PCUICTyping]
prim_size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
prim_val_tag_map [lemma, in MetaRocq.PCUIC.PCUICAst]
prim_val [abbreviation, in MetaRocq.PCUIC.PCUICAst]
prim_tag [inductive, in MetaRocq.Common.Primitive]
prim_depth [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICDepth]
prim_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
prim_pred [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
prim_type_inv [lemma, in MetaRocq.Erasure.EArities]
prim_size [definition, in MetaRocq.Erasure.EInduction]
prim_tag_model_eqdec [instance, in MetaRocq.Erasure.EPrimitive]
prim_val_reflect_eq [instance, in MetaRocq.Erasure.EPrimitive]
prim_model_eqdec [instance, in MetaRocq.Erasure.EPrimitive]
prim_model_reflecteq [instance, in MetaRocq.Erasure.EPrimitive]
prim_model_val [definition, in MetaRocq.Erasure.EPrimitive]
prim_array [definition, in MetaRocq.Erasure.EPrimitive]
prim_string [definition, in MetaRocq.Erasure.EPrimitive]
prim_float [definition, in MetaRocq.Erasure.EPrimitive]
prim_int [definition, in MetaRocq.Erasure.EPrimitive]
prim_val_model [definition, in MetaRocq.Erasure.EPrimitive]
prim_val_tag [definition, in MetaRocq.Erasure.EPrimitive]
prim_val [definition, in MetaRocq.Erasure.EPrimitive]
prim_model_of [definition, in MetaRocq.Erasure.EPrimitive]
prim_model_sind [definition, in MetaRocq.Erasure.EPrimitive]
prim_model_rec [definition, in MetaRocq.Erasure.EPrimitive]
prim_model_ind [definition, in MetaRocq.Erasure.EPrimitive]
prim_model_rect [definition, in MetaRocq.Erasure.EPrimitive]
prim_model [inductive, in MetaRocq.Erasure.EPrimitive]
prim_tag_model_eqdec [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val_reflect_eq [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_eqdec [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_reflecteq [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_val [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_array [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_string [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_float [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_int [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val_model [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val_tag [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_of [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_sind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_rec [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_ind [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_rect [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model [inductive, in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_global_deps [definition, in MetaRocq.Erasure.EAstUtils]
Principality [section, in MetaRocq.PCUIC.PCUICPrincipality]
Principality.cf [variable, in MetaRocq.PCUIC.PCUICPrincipality]
Principality.wfΣ [variable, in MetaRocq.PCUIC.PCUICPrincipality]
Principality.Σ [variable, in MetaRocq.PCUIC.PCUICPrincipality]
principal_type [lemma, in MetaRocq.PCUIC.Bidirectional.BDUnique]
principal_types [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_typing [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_sort_sort [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_type_type [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_sort [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_type [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_type_ind [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
principal_type [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
printConstant [definition, in MetaRocq.Examples.demo]
printConstant' [definition, in MetaRocq.Examples.demo]
printInductive [definition, in MetaRocq.Examples.demo]
PrintTermTree [module, in MetaRocq.Template.Pretty]
PrintTermTree [module, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree [module, in MetaRocq.Erasure.EPretty]
PrintTermTree.env [section, in MetaRocq.Template.Pretty]
PrintTermTree.env [section, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env [section, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.all [variable, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.Aux [section, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.Aux.print_term [variable, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.with_universes [variable, in MetaRocq.Template.Pretty]
_ ^ _ [notation, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.Σ [variable, in MetaRocq.Template.Pretty]
PrintTermTree.env.Σ [variable, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.env.Σ [variable, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.mie_arities_context [definition, in MetaRocq.Template.Pretty]
PrintTermTree.pr [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_program [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_env [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_env_aux [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_mie [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_mib [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_recursivity_kind [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_one_ind_entry [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_one_cstr_entry [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_one_ind [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_one_cstr [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_context [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_term [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_sort [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_defs [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_def [definition, in MetaRocq.Template.Pretty]
PrintTermTree.print_program [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_env [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_env_aux [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_recursivity_kind [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_one_ind [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_one_cstr [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context [abbreviation, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_term [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context_names [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context_gen [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_defs [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_def [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_prim [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_program [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_env [abbreviation, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_global_context [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_decl [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_inductive_body [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_recursivity_kind [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_one_inductive_body [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_constant_body [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_term [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_prim [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_defs [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_def [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_term.Σ [variable, in MetaRocq.Erasure.EPretty]
PrintTermTree.print_term [section, in MetaRocq.Erasure.EPretty]
PrintTermTree.pr_context_decl [definition, in MetaRocq.Template.Pretty]
PrintTermTree.pr_term [abbreviation, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.pr_context_decl [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.pr_allowed_elim [definition, in MetaRocq.Erasure.EPretty]
PrintTermTree.universes_decl_of_universes_entry [definition, in MetaRocq.Template.Pretty]
_ ^ _ [notation, in MetaRocq.Template.Pretty]
_ ^ _ [notation, in MetaRocq.PCUIC.utils.PCUICPretty]
_ ^ _ [notation, in MetaRocq.Erasure.EPretty]
print_constraint_set [definition, in MetaRocq.Common.Universes]
print_constraint_type [definition, in MetaRocq.Common.Universes]
print_lset [definition, in MetaRocq.Common.Universes]
print_universe_instance [definition, in MetaRocq.Common.Universes]
print_program [definition, in MetaRocq.Template.Pretty]
print_env [definition, in MetaRocq.Template.Pretty]
print_term [definition, in MetaRocq.Template.Pretty]
print_mib [definition, in MetaRocq.Template.Pretty]
print_mie [definition, in MetaRocq.Template.Pretty]
print_term.Σ [variable, in MetaRocq.Template.Pretty]
print_term [section, in MetaRocq.Template.Pretty]
print_term [definition, in MetaRocq.Erasure.Typed.ExAst]
print_context_decl [definition, in MetaRocq.SafeChecker.PCUICErrors]
print_term [definition, in MetaRocq.SafeChecker.PCUICErrors]
print_universes_graph [definition, in MetaRocq.SafeChecker.PCUICErrors]
print_edge [definition, in MetaRocq.SafeChecker.PCUICErrors]
print_level [definition, in MetaRocq.SafeChecker.PCUICErrors]
print_list [definition, in MetaRocq.Utils.MRString]
print_nf [definition, in MetaRocq.Template.TemplateMonad.Core]
print_program [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
print_env [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
print_context [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
print_term [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
print_def [definition, in MetaRocq.Common.BasicAst]
print_program [definition, in MetaRocq.Erasure.EPretty]
print_global_context [definition, in MetaRocq.Erasure.EPretty]
ProdNotConvertibleAnn [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ProdNotConvertibleDomains [constructor, in MetaRocq.SafeChecker.PCUICErrors]
product_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Prod_r [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Prod_l [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
prod_r [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
prod_l [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
prod_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
prod_ind [lemma, in MetaRocq.PCUIC.PCUICConfluence]
Prod_conv_cum_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
prod_letin_viewc [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
prod_letin_other [constructor, in MetaRocq.SafeChecker.PCUICSafeChecker]
prod_letin_tLetIn [constructor, in MetaRocq.SafeChecker.PCUICSafeChecker]
prod_letin_tProd [constructor, in MetaRocq.SafeChecker.PCUICSafeChecker]
prod_letin_view [inductive, in MetaRocq.SafeChecker.PCUICSafeChecker]
prod_red_r [constructor, in MetaRocq.Template.Typing]
prod_red_l [constructor, in MetaRocq.Template.Typing]
prod_red_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
prod_red_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
Prod_reflexivity [instance, in MetaRocq.Utils.MRProd]
prod' [record, in MetaRocq.Examples.demo]
program [definition, in MetaRocq.Erasure.EAst]
progress [lemma, in MetaRocq.PCUIC.PCUICProgress]
progress_env_prop [lemma, in MetaRocq.PCUIC.PCUICProgress]
prog_viewc [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_sind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_rec [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_ind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_rect [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_other [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Prim [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_CoFix [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Fix [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Proj [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Case [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Prod [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Lambda [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_Const [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_App [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view [inductive, in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_discr [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
Proj [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
projection [record, in MetaRocq.Common.Kernames]
projection_cumulative_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
projection_context_gen_inst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
projection_subslet [lemma, in MetaRocq.PCUIC.PCUICInductives]
projection_context [definition, in MetaRocq.PCUIC.PCUICInductives]
projection_arg_ctx [definition, in MetaRocq.PCUIC.PCUICInductives]
projection_context_gen [definition, in MetaRocq.PCUIC.PCUICInductives]
projection_decls_type [definition, in MetaRocq.PCUIC.PCUICInductives]
projection_type' [definition, in MetaRocq.PCUIC.PCUICInductives]
projection_type [definition, in MetaRocq.PCUIC.PCUICInductives]
projection_body [record, in MetaRocq.Erasure.EAst]
projP1 [projection, in MetaRocq.Utils.MRPrelude]
projP2 [projection, in MetaRocq.Utils.MRPrelude]
projs_inst_0 [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
projs_subst_above [lemma, in MetaRocq.PCUIC.PCUICInductives]
projs_subst_instance [lemma, in MetaRocq.PCUIC.PCUICInductives]
projs_inst_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
projs_inst_length [lemma, in MetaRocq.PCUIC.PCUICInductives]
projs_inst_skipn [lemma, in MetaRocq.PCUIC.PCUICInductives]
projs_inst_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
projs_inst [definition, in MetaRocq.PCUIC.PCUICInductives]
proj_c [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Proj_Construct_ind_eq [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
Proj_red_cond [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
Proj_Construct_ind_eq [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
proj_red [constructor, in MetaRocq.Template.Typing]
proj_arg [projection, in MetaRocq.Common.Kernames]
proj_npars [projection, in MetaRocq.Common.Kernames]
proj_ind [projection, in MetaRocq.Common.Kernames]
proj_name [projection, in MetaRocq.Erasure.EAst]
proj_red [constructor, in MetaRocq.PCUIC.PCUICReduction]
proj1 [definition, in MetaRocq.Quotation.ToPCUIC.Init]
proj1 [definition, in MetaRocq.Quotation.ToTemplate.Init]
proj1 [definition, in MetaRocq.Utils.MRProd]
proj2 [definition, in MetaRocq.Quotation.ToPCUIC.Init]
proj2 [definition, in MetaRocq.Quotation.ToTemplate.Init]
proj2 [definition, in MetaRocq.Utils.MRProd]
proper_map_ho [instance, in MetaRocq.Utils.MRList]
proper_sort_sup_eq_sort [instance, in MetaRocq.Common.Universes]
proper_univ_sup_eq_univ [instance, in MetaRocq.Common.Universes]
proper_pair_levels_gcs [instance, in MetaRocq.Erasure.ErasureFunction]
Proper_weaken_env_prop_full_gen_respectful [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
Proper_weaken_env_prop_gen_respectful [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
proper_red_ctx [instance, in MetaRocq.PCUIC.PCUICConfluence]
proper_inst' [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
proper_inst [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
proper_add_le_l [instance, in MetaRocq.Utils.MRArith]
proper_add_le_r [instance, in MetaRocq.Utils.MRArith]
proper_S_le [instance, in MetaRocq.Utils.MRArith]
proper_add_lt_l [instance, in MetaRocq.Utils.MRArith]
proper_add_lt_r [instance, in MetaRocq.Utils.MRArith]
proper_S_lt [instance, in MetaRocq.Utils.MRArith]
proper_add_level_edges' [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
proper_add_uctx [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
proper_add_level_edges [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
proper_add_level_edges' [instance, in MetaRocq.Common.uGraph]
proper_add_uctx [instance, in MetaRocq.Common.uGraph]
proper_add_level_edges [instance, in MetaRocq.Common.uGraph]
proper_pair_levels_gcs [instance, in MetaRocq.Common.uGraph]
proper_ext_eq [instance, in MetaRocq.Utils.MRPrelude]
PropLevel [module, in MetaRocq.Common.Universes]
PropLevel.compare [definition, in MetaRocq.Common.Universes]
PropLevel.lProp [constructor, in MetaRocq.Common.Universes]
PropLevel.lSProp [constructor, in MetaRocq.Common.Universes]
PropLevel.lt [definition, in MetaRocq.Common.Universes]
PropLevel.ltSPropProp [constructor, in MetaRocq.Common.Universes]
PropLevel.lt_strorder [instance, in MetaRocq.Common.Universes]
PropLevel.lt__sind [definition, in MetaRocq.Common.Universes]
PropLevel.lt__rec [definition, in MetaRocq.Common.Universes]
PropLevel.lt__ind [definition, in MetaRocq.Common.Universes]
PropLevel.lt__rect [definition, in MetaRocq.Common.Universes]
PropLevel.lt_ [inductive, in MetaRocq.Common.Universes]
PropLevel.t [inductive, in MetaRocq.Common.Universes]
PropLevel.t_sind [definition, in MetaRocq.Common.Universes]
PropLevel.t_rec [definition, in MetaRocq.Common.Universes]
PropLevel.t_ind [definition, in MetaRocq.Common.Universes]
PropLevel.t_rect [definition, in MetaRocq.Common.Universes]
Propositional_Logic_MetaRocq [instance, in MetaRocq.Examples.tauto]
Propositional_Logic_Prop [instance, in MetaRocq.Examples.tauto]
Propositional_Logic [record, in MetaRocq.Examples.tauto]
Prop_ctx [definition, in MetaRocq.Examples.tauto]
prop_sub_type [projection, in MetaRocq.Common.config]
prop_sort_eq [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
Pr' [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
psubst [inductive, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_pred1_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_nth_error_None [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_nth_error' [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_nth_error [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_length' [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_length [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_sind [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_rec [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_ind [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_rect [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_vdef [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_vass [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_empty [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
PTree [module, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE [section, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine_view [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine_view_gen [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_by_tac_eq [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_by_tac [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_direct [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_r [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_l [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.A [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.B [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.C [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.f [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.COMBINE.f_None_None [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.empty [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Empty [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.extensionality [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.extensionality_empty [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine_view [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_by_tac [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_direct [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_r [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_l [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gempty [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.get [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.get' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gmap_filter [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gmap_filter' [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gNode [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gro [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.grs [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gso [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gso_alt_proof [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gso0 [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gss [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gss_alt_proof [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gss0 [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.map_filter [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.map_filter'_opt [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.map_filter' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.MAP_FILTER.B [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.MAP_FILTER.A [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.MAP_FILTER [section, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Nodes [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node001 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node010 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node011 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node100 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node101 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node110 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node111 [constructor, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.not_trivially_empty [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.option_map [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.remove [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.remove' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.rem' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set_Node [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set_Empty [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set0 [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.t [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree [inductive, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_ind [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_ind' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.node [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.empty [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.P [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND.A [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_IND [section, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.node_empty [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_rec [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_rec' [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.node [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.empty [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.B [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC.A [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_REC [section, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.node_empty [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_case [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.node [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.empty [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.B [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE.A [variable, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.TREE_CASE [section, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree' [inductive, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree'_not_empty [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree'_ind [definition, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_rec_gen [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_rec [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_case_gen [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_case [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_map_filter [lemma, in MetaRocq.Utils.canonicaltries.CanonicalTries]
Ptrue [projection, in MetaRocq.Examples.tauto]
Ptyping_sum [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
puinst [projection, in MetaRocq.PCUIC.PCUICAst]
puinst [projection, in MetaRocq.Template.Ast]
pwt [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
pzt [abbreviation, 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) |