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

ParameterEntry [in MetaCoq.Template.Ast]
ParameterEntry [in MetaCoq.PCUIC.PCUICAst]
ParameterEntry [in MetaCoq.Erasure.EAst]
Polymorphic_entry [in MetaCoq.Template.Universes]
Polymorphic_ctx [in MetaCoq.Template.Universes]
positionR_root [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_deep [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_app_lr [in MetaCoq.PCUIC.Syntax.PCUICPosition]
pred_atom_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_prod [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_cofix_congr [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_fix_congr [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_proj_congr [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_case [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_letin [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_app [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_abs [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_proj [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_const [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_delta [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_cofix_proj [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_cofix_case [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_fix [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_iota [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_rel_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_rel_def_unfold [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_zeta [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_beta [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_hole_return [in MetaCoq.PCUIC.Syntax.PCUICPosition]
pred_hole_params [in MetaCoq.PCUIC.Syntax.PCUICPosition]
primFloat [in MetaCoq.PCUIC.utils.PCUICPrimitive]
primFloatModel [in MetaCoq.PCUIC.utils.PCUICPrimitive]
primInt [in MetaCoq.PCUIC.utils.PCUICPrimitive]
primIntModel [in MetaCoq.PCUIC.utils.PCUICPrimitive]
ProdNotConvertibleAnn [in MetaCoq.SafeChecker.PCUICErrors]
ProdNotConvertibleDomains [in MetaCoq.SafeChecker.PCUICErrors]
prod_cons [in MetaCoq.PCUIC.Bidirectional.BDTyping]
prod_red_r [in MetaCoq.Template.Typing]
prod_red_l [in MetaCoq.Template.Typing]
Prod_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Prod_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]
prod_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]
prod_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]
prod_letin_other [in MetaCoq.SafeChecker.PCUICSafeChecker]
prod_letin_tLetIn [in MetaCoq.SafeChecker.PCUICSafeChecker]
prod_letin_tProd [in MetaCoq.SafeChecker.PCUICSafeChecker]
prod_red_r [in MetaCoq.PCUIC.PCUICReduction]
prod_red_l [in MetaCoq.PCUIC.PCUICReduction]
prog_view_other [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_CoFix [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Fix [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Proj [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Case [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Prod [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Lambda [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Const [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_App [in MetaCoq.SafeChecker.PCUICSafeConversion]
Proj [in MetaCoq.PCUIC.Syntax.PCUICPosition]
proj_red [in MetaCoq.Template.Typing]
proj_c [in MetaCoq.PCUIC.Syntax.PCUICPosition]
proj_red [in MetaCoq.PCUIC.PCUICReduction]
PropLevel.lProp [in MetaCoq.Template.Universes]
PropLevel.lSProp [in MetaCoq.Template.Universes]
PropLevel.ltSPropProp [in MetaCoq.Template.Universes]
psubst_vdef [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_vass [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_empty [in MetaCoq.PCUIC.PCUICParallelReduction]



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)