| 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 (lemma)
params_subslet [in MetaRocq.PCUIC.PCUICNormal]PathOf_proper_weight [in MetaRocq.Common.uGraph]
PathOf_proper [in MetaRocq.Common.uGraph]
pcuic_canonicity [in MetaRocq.PCUIC.PCUICCanonicity]
pcuic_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
pcuic_function_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pcuic_eval_function [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pcuic_consistent [in MetaRocq.PCUIC.PCUICConsistency]
pcuic_to_template [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
permute_lift0 [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
permute_lift [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
permute_lift0 [in MetaRocq.Template.LiftSubst]
permute_lift [in MetaRocq.Template.LiftSubst]
permute_lift0 [in MetaRocq.Erasure.ELiftSubst]
permute_lift [in MetaRocq.Erasure.ELiftSubst]
pick_hyp_def [in MetaRocq.Examples.tauto]
plookup_env_extends [in MetaRocq.PCUIC.PCUICFirstorder]
plookup_env_Some_not_fresh [in MetaRocq.PCUIC.PCUICFirstorder]
plookup_env_lookup_env [in MetaRocq.PCUIC.PCUICFirstorder]
plus_minus' [in MetaRocq.PCUIC.Syntax.PCUICClosed]
poscat_valid [in MetaRocq.PCUIC.Syntax.PCUICPosition]
poscat_atpos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_stack_pos_xpos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_xposition_inv [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_context_position_inv [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_poscat_nonil [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_trans [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positionR_poscat [in MetaRocq.PCUIC.Syntax.PCUICPosition]
positive_cstr_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_arg_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_smash_middle [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_closed_indices' [in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_args [in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_args_subst_arities [in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_arg_subst [in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_arg_subst_instance [in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
positive_cstr_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICInductiveInversion]
posR_trans [in MetaRocq.PCUIC.Syntax.PCUICPosition]
posR_Acc [in MetaRocq.PCUIC.Syntax.PCUICPosition]
precompose_subst_instance_global [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precond [in MetaRocq.ErasurePlugin.ErasureCorrectness]
precond2 [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pred_red [in MetaRocq.PCUIC.PCUICConfluence]
pred_rel_confluent [in MetaRocq.PCUIC.PCUICConfluence]
pred_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
pred_atom_inst [in MetaRocq.PCUIC.PCUICParallelReduction]
pred_subst_rho_fix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_subst_rho_cofix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_mkApps [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_snd_nth [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred_atom_mkApps [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_rel_alpha_confluent [in MetaRocq.PCUIC.PCUICConfluence]
pred1_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
pred1_upto_names_gen [in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel_alpha_red1_rel_alpha [in MetaRocq.PCUIC.PCUICConfluence]
pred1_red' [in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_red_ctx [in MetaRocq.PCUIC.PCUICConfluence]
pred1_rel_confluent [in MetaRocq.PCUIC.PCUICConfluence]
pred1_on_free_vars_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICConfluence]
pred1_red_r [in MetaRocq.PCUIC.PCUICConfluence]
pred1_pred1_r' [in MetaRocq.PCUIC.PCUICConfluence]
pred1_pred1_r [in MetaRocq.PCUIC.PCUICConfluence]
pred1_red_r_gen' [in MetaRocq.PCUIC.PCUICConfluence]
pred1_red_r_gen [in MetaRocq.PCUIC.PCUICConfluence]
pred1_red [in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_pred1_inv [in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_over_assumption_context [in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_assumption_context [in MetaRocq.PCUIC.PCUICConfluence]
pred1_ctx_pred1 [in MetaRocq.PCUIC.PCUICConfluence]
pred1_subst_context [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_up [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_Upn [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_vdef_Up [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_Up [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_ext [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_subst_pred1_ctx [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_rename [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx_over_refl [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_refl [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ctx_refl [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_refl_gen [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_pred1_ctx [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_ind_all_ctx [in MetaRocq.PCUIC.PCUICParallelReduction]
pred1_diamond [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_ctx_over_inst_case_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_ctx_over_refl_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_expand_lets [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_ext [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_subst_consn [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_rho_fix_context_2 [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_fix_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_mfix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_over_on_ctx_free_vars [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_ctx_free_vars [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_mfix_ind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tCoFix_refl_inv [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tCoFix_inv [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tFix_refl_inv [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tFix_inv [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tConst_axiom [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tRel [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tInd [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_refl_tConstruct [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tConstruct [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pres_let_bodies_ctx_refl [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
pres_let_bodies_assumption_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
pres_inductives_lookup [in MetaRocq.ErasurePlugin.ErasureCorrectness]
pres_bodies_rename' [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies_rename [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies_inst_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
pre_case_predicate_context_gen_eq [in MetaRocq.PCUIC.PCUICElimination]
pre_type_mkApps_arity [in MetaRocq.PCUIC.PCUICSpine]
pre_case_branch_context_eq [in MetaRocq.PCUIC.PCUICInductiveInversion]
pre_case_branch_context_length_args [in MetaRocq.PCUIC.PCUICCasesContexts]
Pre_glob [in MetaRocq.Erasure.EOptimizePropDiscr]
Pre_glob [in MetaRocq.Erasure.EConstructorsAsBlocks]
pre_remove_match_on_box_typed_fresh [in MetaRocq.ErasurePlugin.ETransform]
Pre_glob [in MetaRocq.Erasure.EInlineProjections]
pre_case_branch_context_gen_length [in MetaRocq.PCUIC.PCUICCasesHelper]
pre_case_predicate_context_gen_indpred_ctx [in MetaRocq.PCUIC.PCUICCasesHelper]
primitive_invariants_axiom [in MetaRocq.Erasure.EArities]
primProp_mapu_id [in MetaRocq.PCUIC.PCUICAst]
primProp_map_inv [in MetaRocq.PCUIC.PCUICAst]
primProp_map [in MetaRocq.PCUIC.PCUICAst]
primProp_test_prim [in MetaRocq.PCUIC.PCUICAst]
primProp_map_id [in MetaRocq.PCUIC.PCUICAst]
primProp_map_eq [in MetaRocq.PCUIC.PCUICAst]
primProp_map [in MetaRocq.Erasure.EPrimitive]
primProp_impl [in MetaRocq.Erasure.EPrimitive]
primProp_conj [in MetaRocq.Erasure.EPrimitive]
primProp_impl_test_prim [in MetaRocq.Erasure.EPrimitive]
prim_val_tag_map [in MetaRocq.PCUIC.PCUICAst]
prim_type_inv [in MetaRocq.Erasure.EArities]
principal_type [in MetaRocq.PCUIC.Bidirectional.BDUnique]
principal_types [in MetaRocq.SafeChecker.PCUICSafeRetyping]
principal_type_ind [in MetaRocq.PCUIC.PCUICPrincipality]
principal_type [in MetaRocq.PCUIC.PCUICPrincipality]
product_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
prod_ind [in MetaRocq.PCUIC.PCUICConfluence]
Prod_conv_cum_inv [in MetaRocq.PCUIC.PCUICConversion]
progress [in MetaRocq.PCUIC.PCUICProgress]
progress_env_prop [in MetaRocq.PCUIC.PCUICProgress]
projection_cumulative_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
projection_context_gen_inst [in MetaRocq.PCUIC.PCUICInductiveInversion]
projection_subslet [in MetaRocq.PCUIC.PCUICInductives]
projs_inst_0 [in MetaRocq.PCUIC.PCUICInductiveInversion]
projs_subst_above [in MetaRocq.PCUIC.PCUICInductives]
projs_subst_instance [in MetaRocq.PCUIC.PCUICInductives]
projs_inst_lift [in MetaRocq.PCUIC.PCUICInductives]
projs_inst_length [in MetaRocq.PCUIC.PCUICInductives]
projs_inst_skipn [in MetaRocq.PCUIC.PCUICInductives]
projs_inst_subst [in MetaRocq.PCUIC.PCUICInductives]
Proj_Construct_ind_eq [in MetaRocq.PCUIC.PCUICSafeLemmata]
Proj_red_cond [in MetaRocq.PCUIC.PCUICSafeLemmata]
Proj_Construct_ind_eq [in MetaRocq.PCUIC.PCUICInductiveInversion]
prop_sort_eq [in MetaRocq.PCUIC.PCUICCumulProp]
psubst_pred1_subst [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_nth_error_None [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_nth_error' [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_nth_error [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_length' [in MetaRocq.PCUIC.PCUICParallelReduction]
psubst_length [in MetaRocq.PCUIC.PCUICParallelReduction]
PTree.combine'_by_tac_eq [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.extensionality [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.extensionality_empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine_view [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_by_tac [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_direct [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_r [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gcombine'_l [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gempty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gmap_filter [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gmap_filter' [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gNode [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gro [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.grs [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gso [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gso_alt_proof [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gso0 [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gss [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gss_alt_proof [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.gss0 [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set_Node [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.set_Empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.tree'_not_empty [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_rec_gen [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_rec [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_case_gen [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_tree_case [in MetaRocq.Utils.canonicaltries.CanonicalTries]
PTree.unroll_map_filter [in MetaRocq.Utils.canonicaltries.CanonicalTries]
| 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) |