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 (definition)

parens [in MetaRocq.Utils.MRString]
pb_of_dec [in MetaRocq.Quotation.CommonUtils]
pclengths [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
PCUICConversionParAlgo.cumul_gen [in MetaRocq.PCUIC.PCUICCumulativity]
PCUICConversionParSpec.cumul_gen [in MetaRocq.PCUIC.PCUICCumulativitySpec]
PCUICTermUtils.destArity [in MetaRocq.PCUIC.PCUICAst]
PCUICTermUtils.inds [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.closedn [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.lift [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.mkApps [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.noccur_between [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.subst [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.subst_instance_constr [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.term [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tInd [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tLambda [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tLetIn [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tProd [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tProj [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tRel [in MetaRocq.PCUIC.PCUICAst]
PCUICTerm.tSort [in MetaRocq.PCUIC.PCUICAst]
PCUICTypingDef.typing [in MetaRocq.PCUIC.PCUICTyping]
pcuic_program [in MetaRocq.PCUIC.PCUICProgram]
pcuic_lookup_inductive_pars [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pcuic_expand_lets_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
pcuic_expand_lets_transform [in MetaRocq.TemplatePCUIC.PCUICTransform]
pick_hyp [in MetaRocq.Examples.tauto]
pi_block [in MetaRocq.Template.Lib]
pi_ctors [in MetaRocq.Template.Lib]
plengths [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
plengths [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
plookup_env [in MetaRocq.PCUIC.PCUICFirstorder]
polymorphic_instance [in MetaRocq.Common.Universes]
polymorphic_constraints [in MetaRocq.Template.Checker]
pos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
position [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_sind [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_ind [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positive_sind [in MetaRocq.Utils.canonicaltries.String2pos]
positive_rec [in MetaRocq.Utils.canonicaltries.String2pos]
positive_ind [in MetaRocq.Utils.canonicaltries.String2pos]
positive_rect [in MetaRocq.Utils.canonicaltries.String2pos]
posR [in MetaRocq.PCUIC.Syntax.PCUICPosition]
post_dearging_checks [in MetaRocq.ErasurePlugin.ETransform]
pos_of_string [in MetaRocq.Utils.canonicaltries.String2pos]
Pr [in MetaRocq.SafeChecker.PCUICSafeReduce]
pr [in MetaRocq.Erasure.EPretty]
prec [in MetaRocq.Common.BasicAst]
precompose_subst_instance_global__2 [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance_global__1 [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance__2 [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance__1 [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
predA [in MetaRocq.Utils.MRPred]
predA [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
predicate_hole_pars [in MetaRocq.PCUIC.Syntax.PCUICPosition]
predicate_hole_context [in MetaRocq.PCUIC.Syntax.PCUICPosition]
predicate_size [in MetaRocq.Examples.tauto]
predicate_size [in MetaRocq.PCUIC.utils.PCUICSize]
predicate_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
pred_atom [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rel_alpha [in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel [in MetaRocq.PCUIC.PCUICConfluence]
pred1_subst [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_sind [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rec [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ind [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rect [in MetaRocq.PCUIC.PCUICParallelReduction]
preserves_expansion_env [in MetaRocq.ErasurePlugin.ETransform]
preserves_expansion [in MetaRocq.ErasurePlugin.ETransform]
pres_let_bodies [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_bodies [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pretty_string_of_branch [in MetaRocq.PCUIC.PCUICAst]
pretty_string_of_branch [in MetaRocq.Template.Ast]
Pre_glob [in MetaRocq.Erasure.EGenericGlobalMap]
Pre_decl [in MetaRocq.Erasure.EGenericGlobalMap]
pre_case_branch_context [in MetaRocq.PCUIC.PCUICCasesContexts]
Pre_glob [in MetaRocq.Erasure.EGenericMapEnv]
Pre_decl [in MetaRocq.Erasure.EGenericMapEnv]
pre_remove_match_on_box_typed [in MetaRocq.ErasurePlugin.ETransform]
pre_erasure_pipeline_mapping [in MetaRocq.ErasurePlugin.Erasure]
pre_erasure_pipeline [in MetaRocq.ErasurePlugin.Erasure]
pre_case_branch_context_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
pre_case_predicate_context_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
pre_case_predicate_context_gen [in MetaRocq.Template.Ast]
primitive_typing_hyps_size [in MetaRocq.PCUIC.PCUICTyping]
primProp_sind [in MetaRocq.Erasure.EPrimitive]
primProp_rec [in MetaRocq.Erasure.EPrimitive]
primProp_ind [in MetaRocq.Erasure.EPrimitive]
primProp_rect [in MetaRocq.Erasure.EPrimitive]
prim_type [in MetaRocq.PCUIC.PCUICTyping]
prim_size [in MetaRocq.PCUIC.utils.PCUICSize]
prim_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
prim_size [in MetaRocq.Erasure.EInduction]
prim_model_val [in MetaRocq.Erasure.EPrimitive]
prim_array [in MetaRocq.Erasure.EPrimitive]
prim_string [in MetaRocq.Erasure.EPrimitive]
prim_float [in MetaRocq.Erasure.EPrimitive]
prim_int [in MetaRocq.Erasure.EPrimitive]
prim_val_model [in MetaRocq.Erasure.EPrimitive]
prim_val_tag [in MetaRocq.Erasure.EPrimitive]
prim_val [in MetaRocq.Erasure.EPrimitive]
prim_model_of [in MetaRocq.Erasure.EPrimitive]
prim_model_sind [in MetaRocq.Erasure.EPrimitive]
prim_model_rec [in MetaRocq.Erasure.EPrimitive]
prim_model_ind [in MetaRocq.Erasure.EPrimitive]
prim_model_rect [in MetaRocq.Erasure.EPrimitive]
prim_model_val [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_array [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_string [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_float [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_int [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val_model [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val_tag [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_val [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_of [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_sind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_rec [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_ind [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_model_rect [in MetaRocq.PCUIC.utils.PCUICPrimitive]
prim_global_deps [in MetaRocq.Erasure.EAstUtils]
principal_typing [in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_sort_sort [in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_type_type [in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_sort [in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_type [in MetaRocq.SafeChecker.PCUICSafeRetyping]
printConstant [in MetaRocq.Examples.demo]
printConstant' [in MetaRocq.Examples.demo]
printInductive [in MetaRocq.Examples.demo]
PrintTermTree.mie_arities_context [in MetaRocq.Template.Pretty]
PrintTermTree.pr [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_program [in MetaRocq.Template.Pretty]
PrintTermTree.print_env [in MetaRocq.Template.Pretty]
PrintTermTree.print_env_aux [in MetaRocq.Template.Pretty]
PrintTermTree.print_mie [in MetaRocq.Template.Pretty]
PrintTermTree.print_mib [in MetaRocq.Template.Pretty]
PrintTermTree.print_recursivity_kind [in MetaRocq.Template.Pretty]
PrintTermTree.print_one_ind_entry [in MetaRocq.Template.Pretty]
PrintTermTree.print_one_cstr_entry [in MetaRocq.Template.Pretty]
PrintTermTree.print_one_ind [in MetaRocq.Template.Pretty]
PrintTermTree.print_one_cstr [in MetaRocq.Template.Pretty]
PrintTermTree.print_context [in MetaRocq.Template.Pretty]
PrintTermTree.print_term [in MetaRocq.Template.Pretty]
PrintTermTree.print_sort [in MetaRocq.Template.Pretty]
PrintTermTree.print_defs [in MetaRocq.Template.Pretty]
PrintTermTree.print_def [in MetaRocq.Template.Pretty]
PrintTermTree.print_program [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_env [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_env_aux [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_recursivity_kind [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_one_ind [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_one_cstr [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_term [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context_names [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context_gen [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_defs [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_def [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_prim [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_program [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_global_context [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_decl [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_inductive_body [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_recursivity_kind [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_one_inductive_body [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_constant_body [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_term [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_prim [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_defs [in MetaRocq.Erasure.EPretty]
PrintTermTree.print_def [in MetaRocq.Erasure.EPretty]
PrintTermTree.pr_context_decl [in MetaRocq.Template.Pretty]
PrintTermTree.pr_context_decl [in MetaRocq.PCUIC.utils.PCUICPretty]
PrintTermTree.pr_allowed_elim [in MetaRocq.Erasure.EPretty]
PrintTermTree.universes_decl_of_universes_entry [in MetaRocq.Template.Pretty]
print_constraint_set [in MetaRocq.Common.Universes]
print_constraint_type [in MetaRocq.Common.Universes]
print_lset [in MetaRocq.Common.Universes]
print_universe_instance [in MetaRocq.Common.Universes]
print_program [in MetaRocq.Template.Pretty]
print_env [in MetaRocq.Template.Pretty]
print_term [in MetaRocq.Template.Pretty]
print_mib [in MetaRocq.Template.Pretty]
print_mie [in MetaRocq.Template.Pretty]
print_term [in MetaRocq.Erasure.Typed.ExAst]
print_context_decl [in MetaRocq.SafeChecker.PCUICErrors]
print_term [in MetaRocq.SafeChecker.PCUICErrors]
print_universes_graph [in MetaRocq.SafeChecker.PCUICErrors]
print_edge [in MetaRocq.SafeChecker.PCUICErrors]
print_level [in MetaRocq.SafeChecker.PCUICErrors]
print_list [in MetaRocq.Utils.MRString]
print_nf [in MetaRocq.Template.TemplateMonad.Core]
print_program [in MetaRocq.PCUIC.utils.PCUICPretty]
print_env [in MetaRocq.PCUIC.utils.PCUICPretty]
print_context [in MetaRocq.PCUIC.utils.PCUICPretty]
print_term [in MetaRocq.PCUIC.utils.PCUICPretty]
print_def [in MetaRocq.Common.BasicAst]
print_program [in MetaRocq.Erasure.EPretty]
print_global_context [in MetaRocq.Erasure.EPretty]
prod_letin_viewc [in MetaRocq.SafeChecker.PCUICSafeChecker]
program [in MetaRocq.Erasure.EAst]
prog_viewc [in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_sind [in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_rec [in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_ind [in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_view_rect [in MetaRocq.SafeChecker.PCUICSafeConversion]
prog_discr [in MetaRocq.SafeChecker.PCUICSafeConversion]
projection_context [in MetaRocq.PCUIC.PCUICInductives]
projection_arg_ctx [in MetaRocq.PCUIC.PCUICInductives]
projection_context_gen [in MetaRocq.PCUIC.PCUICInductives]
projection_decls_type [in MetaRocq.PCUIC.PCUICInductives]
projection_type' [in MetaRocq.PCUIC.PCUICInductives]
projection_type [in MetaRocq.PCUIC.PCUICInductives]
projs_inst [in MetaRocq.PCUIC.PCUICInductives]
proj1 [in MetaRocq.Quotation.ToPCUIC.Init]
proj1 [in MetaRocq.Quotation.ToTemplate.Init]
proj1 [in MetaRocq.Utils.MRProd]
proj2 [in MetaRocq.Quotation.ToPCUIC.Init]
proj2 [in MetaRocq.Quotation.ToTemplate.Init]
proj2 [in MetaRocq.Utils.MRProd]
PropLevel.compare [in MetaRocq.Common.Universes]
PropLevel.lt [in MetaRocq.Common.Universes]
PropLevel.lt__sind [in MetaRocq.Common.Universes]
PropLevel.lt__rec [in MetaRocq.Common.Universes]
PropLevel.lt__ind [in MetaRocq.Common.Universes]
PropLevel.lt__rect [in MetaRocq.Common.Universes]
PropLevel.t_sind [in MetaRocq.Common.Universes]
PropLevel.t_rec [in MetaRocq.Common.Universes]
PropLevel.t_ind [in MetaRocq.Common.Universes]
PropLevel.t_rect [in MetaRocq.Common.Universes]
Prop_ctx [in MetaRocq.Examples.tauto]
Pr' [in MetaRocq.SafeChecker.PCUICSafeReduce]
psubst_sind [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_rec [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_ind [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_rect [in MetaRocq.PCUIC.PCUICParallelReduction]
PTree.combine [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine_view [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine_view_gen [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_by_tac [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_direct [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_r [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.combine'_l [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.get [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.get' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.map_filter [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.map_filter'_opt [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.map_filter' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.Node [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.not_trivially_empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.option_map [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.remove [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.remove' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.rem' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set0 [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.t [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_ind [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_ind' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_rec [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_rec' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree_case [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree'_ind [in MetaRocq.Utils.canonicaltries.CanonicalTries]
Ptyping_sum [in MetaRocq.PCUIC.Bidirectional.BDTyping]



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)