| 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 | (75519 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 | (245 entries) |
| Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
P (definition)
pack [in MetaCoq.Translations.sigma]pack [in MetaCoq.Translations.param_generous_packed]
pair [in MetaCoq.Translations.sigma]
pair [in MetaCoq.Translations.param_generous_packed]
pairTrue [in MetaCoq.Translations.times_bool_fun]
parens [in MetaCoq.Template.utils.MCString]
paths [in MetaCoq.Translations.MiniHoTT]
paths_ind_beta [in MetaCoq.Translations.MiniHoTT]
paths_ind [in MetaCoq.Translations.MiniHoTT]
paths_ind_beta [in MetaCoq.Translations.MiniHoTT_paths]
paths_ind [in MetaCoq.Translations.MiniHoTT_paths]
path_equiv [in MetaCoq.Translations.MiniHoTT]
path_unit [in MetaCoq.Translations.MiniHoTT]
path_path_sigma [in MetaCoq.Translations.MiniHoTT]
path_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT]
path_sigma_p1_1p' [in MetaCoq.Translations.MiniHoTT]
path_sigma_pp_pp' [in MetaCoq.Translations.MiniHoTT]
path_sigma_pp_pp [in MetaCoq.Translations.MiniHoTT]
path_sigma' [in MetaCoq.Translations.MiniHoTT]
path_sigma_uncurried_contra [in MetaCoq.Translations.MiniHoTT]
path_sigma [in MetaCoq.Translations.MiniHoTT]
path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT]
path_forall_V [in MetaCoq.Translations.MiniHoTT]
path_forall_pp [in MetaCoq.Translations.MiniHoTT]
path_forall_1 [in MetaCoq.Translations.MiniHoTT]
path_basedpaths' [in MetaCoq.Translations.MiniHoTT]
path_basedpaths [in MetaCoq.Translations.MiniHoTT]
path_contr [in MetaCoq.Translations.MiniHoTT]
path_forall2 [in MetaCoq.Translations.MiniHoTT]
path_forall [in MetaCoq.Translations.MiniHoTT]
path_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
path_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma_p1_1p' [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma_pp_pp' [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma_pp_pp [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma' [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma_uncurried_contra [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT_paths]
path_forall_V [in MetaCoq.Translations.MiniHoTT_paths]
path_forall_pp [in MetaCoq.Translations.MiniHoTT_paths]
path_forall_1 [in MetaCoq.Translations.MiniHoTT_paths]
path_basedpaths' [in MetaCoq.Translations.MiniHoTT_paths]
path_basedpaths [in MetaCoq.Translations.MiniHoTT_paths]
path_contr [in MetaCoq.Translations.MiniHoTT_paths]
path_forall2 [in MetaCoq.Translations.MiniHoTT_paths]
path_forall [in MetaCoq.Translations.MiniHoTT_paths]
path2_contr [in MetaCoq.Translations.MiniHoTT]
path2_contr [in MetaCoq.Translations.MiniHoTT_paths]
pclengths [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Pclosed [in MetaCoq.PCUIC.Syntax.PCUICClosed]
PCUICConversionParAlgo.cumul_gen [in MetaCoq.PCUIC.PCUICCumulativity]
PCUICConversionParSpec.cumul_gen [in MetaCoq.PCUIC.PCUICCumulativitySpec]
PCUICTermUtils.destArity [in MetaCoq.PCUIC.PCUICAst]
PCUICTermUtils.inds [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.closedn [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.lift [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.mkApps [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.noccur_between [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.subst [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.subst_instance_constr [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.term [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tInd [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tLambda [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tLetIn [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tProd [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tProj [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tRel [in MetaCoq.PCUIC.PCUICAst]
PCUICTerm.tSort [in MetaCoq.PCUIC.PCUICAst]
PCUICTypingDef.typing [in MetaCoq.PCUIC.PCUICTyping]
pcuic_expand_lets_transform [in MetaCoq.PCUIC.PCUICTransform]
pcuic_program [in MetaCoq.PCUIC.PCUICProgram]
pentagon [in MetaCoq.Translations.MiniHoTT]
pentagon [in MetaCoq.Translations.MiniHoTT_paths]
pick_hyp [in MetaCoq.Examples.tauto]
plengths [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
plengths [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
plookup_env [in MetaCoq.PCUIC.PCUICFirstorder]
pointwise_paths [in MetaCoq.Translations.MiniHoTT]
pointwise_paths [in MetaCoq.Translations.MiniHoTT_paths]
polymorphic_instance [in MetaCoq.Template.Universes]
polymorphic_constraints [in MetaCoq.Template.Checker]
pos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
position [in MetaCoq.PCUIC.Syntax.PCUICPosition]
posR [in MetaCoq.PCUIC.Syntax.PCUICPosition]
postcomposeequiv_αequiv [in MetaCoq.Translations.times_bool_fun2]
postcompose_equiv [in MetaCoq.Translations.times_bool_fun2]
pouet [in MetaCoq.Translations.times_bool_fun]
pr [in MetaCoq.Erasure.EPretty]
Pr [in MetaCoq.SafeChecker.PCUICSafeReduce]
prec [in MetaCoq.Template.BasicAst]
precompose_subst_instance_global__2 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance_global__1 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance__2 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance__1 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
predA [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
predA [in MetaCoq.Template.utils.MCPred]
predicate_hole_pars [in MetaCoq.PCUIC.Syntax.PCUICPosition]
predicate_hole_context [in MetaCoq.PCUIC.Syntax.PCUICPosition]
predicate_size [in MetaCoq.Examples.tauto]
predicate_size [in MetaCoq.PCUIC.utils.PCUICSize]
predicate_depth_gen [in MetaCoq.PCUIC.Syntax.PCUICDepth]
pred_atom [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_rel_alpha [in MetaCoq.PCUIC.PCUICConfluence]
pred1_rel [in MetaCoq.PCUIC.PCUICConfluence]
pres_let_bodies [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
pres_bodies [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pretty_string_of_branch [in MetaCoq.Template.Ast]
pretty_string_of_branch [in MetaCoq.PCUIC.PCUICAst]
pre_case_predicate_context_gen [in MetaCoq.Template.Ast]
pre_case_branch_context_gen [in MetaCoq.PCUIC.Syntax.PCUICCases]
pre_case_predicate_context_gen [in MetaCoq.PCUIC.Syntax.PCUICCases]
pre_case_branch_context [in MetaCoq.PCUIC.PCUICCasesContexts]
Pre_glob [in MetaCoq.Erasure.EGenericMapEnv]
Pre_decl [in MetaCoq.Erasure.EGenericMapEnv]
prim_model_val [in MetaCoq.PCUIC.utils.PCUICPrimitive]
prim_val_model [in MetaCoq.PCUIC.utils.PCUICPrimitive]
prim_val_tag [in MetaCoq.PCUIC.utils.PCUICPrimitive]
prim_val [in MetaCoq.PCUIC.utils.PCUICPrimitive]
prim_model_of [in MetaCoq.PCUIC.utils.PCUICPrimitive]
principal_typing [in MetaCoq.SafeChecker.PCUICSafeRetyping]
principal_sort_sort [in MetaCoq.SafeChecker.PCUICSafeRetyping]
principal_type_type [in MetaCoq.SafeChecker.PCUICSafeRetyping]
principal_sort [in MetaCoq.SafeChecker.PCUICSafeRetyping]
principal_type [in MetaCoq.SafeChecker.PCUICSafeRetyping]
printConstant [in MetaCoq.Examples.demo]
printConstant' [in MetaCoq.Examples.demo]
printInductive [in MetaCoq.Examples.demo]
PrintTermTree.mie_arities_context [in MetaCoq.Template.Pretty]
PrintTermTree.pr [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_program [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_global_context [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_decl [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_inductive_body [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_one_inductive_body [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_constant_body [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_term [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_defs [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_def [in MetaCoq.Erasure.EPretty]
PrintTermTree.print_program [in MetaCoq.Template.Pretty]
PrintTermTree.print_env [in MetaCoq.Template.Pretty]
PrintTermTree.print_env_aux [in MetaCoq.Template.Pretty]
PrintTermTree.print_mie [in MetaCoq.Template.Pretty]
PrintTermTree.print_mib [in MetaCoq.Template.Pretty]
PrintTermTree.print_one_ind_entry [in MetaCoq.Template.Pretty]
PrintTermTree.print_one_cstr_entry [in MetaCoq.Template.Pretty]
PrintTermTree.print_one_ind [in MetaCoq.Template.Pretty]
PrintTermTree.print_one_cstr [in MetaCoq.Template.Pretty]
PrintTermTree.print_context [in MetaCoq.Template.Pretty]
PrintTermTree.print_term [in MetaCoq.Template.Pretty]
PrintTermTree.print_universe [in MetaCoq.Template.Pretty]
PrintTermTree.print_defs [in MetaCoq.Template.Pretty]
PrintTermTree.print_def [in MetaCoq.Template.Pretty]
PrintTermTree.print_program [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_env [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_env_aux [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_one_ind [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_one_cstr [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_term [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context_names [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_context_gen [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_defs [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.print_def [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.pr_allowed_elim [in MetaCoq.Erasure.EPretty]
PrintTermTree.pr_context_decl [in MetaCoq.Template.Pretty]
PrintTermTree.pr_context_decl [in MetaCoq.PCUIC.utils.PCUICPretty]
PrintTermTree.universes_decl_of_universes_entry [in MetaCoq.Template.Pretty]
print_constraint_set [in MetaCoq.Template.Universes]
print_constraint_type [in MetaCoq.Template.Universes]
print_lset [in MetaCoq.Template.Universes]
print_universe_instance [in MetaCoq.Template.Universes]
print_def [in MetaCoq.Template.BasicAst]
print_nf [in MetaCoq.Template.TemplateMonad.Core]
print_program [in MetaCoq.Erasure.EPretty]
print_global_context [in MetaCoq.Erasure.EPretty]
print_list [in MetaCoq.Template.utils.MCString]
print_context_decl [in MetaCoq.SafeChecker.PCUICErrors]
print_term [in MetaCoq.SafeChecker.PCUICErrors]
print_universes_graph [in MetaCoq.SafeChecker.PCUICErrors]
print_edge [in MetaCoq.SafeChecker.PCUICErrors]
print_level [in MetaCoq.SafeChecker.PCUICErrors]
print_program [in MetaCoq.Template.Pretty]
print_env [in MetaCoq.Template.Pretty]
print_term [in MetaCoq.Template.Pretty]
print_mib [in MetaCoq.Template.Pretty]
print_mie [in MetaCoq.Template.Pretty]
print_program [in MetaCoq.PCUIC.utils.PCUICPretty]
print_env [in MetaCoq.PCUIC.utils.PCUICPretty]
print_context [in MetaCoq.PCUIC.utils.PCUICPretty]
print_term [in MetaCoq.PCUIC.utils.PCUICPretty]
prod_letin_viewc [in MetaCoq.SafeChecker.PCUICSafeChecker]
program [in MetaCoq.Erasure.EAst]
prog_viewc [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_discr [in MetaCoq.SafeChecker.PCUICSafeConversion]
proj [in MetaCoq.Translations.sigma]
proj [in MetaCoq.Translations.param_generous_packed]
projection_context [in MetaCoq.PCUIC.PCUICInductives]
projection_arg_ctx [in MetaCoq.PCUIC.PCUICInductives]
projection_context_gen [in MetaCoq.PCUIC.PCUICInductives]
projection_decls_type [in MetaCoq.PCUIC.PCUICInductives]
projection_type' [in MetaCoq.PCUIC.PCUICInductives]
projection_type [in MetaCoq.PCUIC.PCUICInductives]
projs_inst [in MetaCoq.PCUIC.PCUICInductives]
proj1 [in MetaCoq.Translations.times_bool_fun]
proj1 [in MetaCoq.Translations.sigma]
proj1 [in MetaCoq.Translations.param_generous_packed]
proj2 [in MetaCoq.Translations.times_bool_fun]
proj2 [in MetaCoq.Translations.sigma]
proj2 [in MetaCoq.Translations.param_generous_packed]
property [in MetaCoq.Template.Typing]
property [in MetaCoq.PCUIC.PCUICTyping]
PropLevel.compare [in MetaCoq.Template.Universes]
PropLevel.lt [in MetaCoq.Template.Universes]
Prop_univ [in MetaCoq.SafeChecker.PCUICConsistency]
Prop_ctx [in MetaCoq.Examples.tauto]
Pr' [in MetaCoq.SafeChecker.PCUICSafeReduce]
pr1_path_V [in MetaCoq.Translations.MiniHoTT]
pr1_path_pp [in MetaCoq.Translations.MiniHoTT]
pr1_path_1 [in MetaCoq.Translations.MiniHoTT]
pr1_path_sigma [in MetaCoq.Translations.MiniHoTT]
pr1_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT]
pr1_path [in MetaCoq.Translations.MiniHoTT]
pr1_path_V [in MetaCoq.Translations.MiniHoTT_paths]
pr1_path_pp [in MetaCoq.Translations.MiniHoTT_paths]
pr1_path_1 [in MetaCoq.Translations.MiniHoTT_paths]
pr1_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
pr1_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT_paths]
pr1_path [in MetaCoq.Translations.MiniHoTT_paths]
pr2_path_sigma [in MetaCoq.Translations.MiniHoTT]
pr2_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT]
pr2_path [in MetaCoq.Translations.MiniHoTT]
pr2_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
pr2_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT_paths]
pr2_path [in MetaCoq.Translations.MiniHoTT_paths]
Ptyping_sum [in MetaCoq.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 | (75519 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 | (245 entries) |
| Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |