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)

F (constructor)

Fa [in MetaRocq.Examples.tauto]
Fallback [in MetaRocq.SafeChecker.PCUICSafeConversion]
Finite [in MetaRocq.Common.BasicAst]
firstorder_spine_cons [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_nil [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_C [in MetaRocq.PCUIC.PCUICFirstorder]
Fix [in MetaRocq.PCUIC.Syntax.PCUICPosition]
Fix [in MetaRocq.PCUIC.PCUICTyping]
FixMfixMismatch [in MetaRocq.SafeChecker.PCUICErrors]
FixRargMismatch [in MetaRocq.SafeChecker.PCUICErrors]
Fix_app [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_mfix_bd [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_mfix_ty [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_lambda_other [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_fix [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_lambda [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_other [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_lambda [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_fix [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_red_body [in MetaRocq.Template.Typing]
fix_red_ty [in MetaRocq.Template.Typing]
fix_red_body [in MetaRocq.PCUIC.PCUICReduction]
fix_red_ty [in MetaRocq.PCUIC.PCUICReduction]
Forall_type_spine_cons [in MetaRocq.Template.Typing]
Forall_type_spine_nil [in MetaRocq.Template.Typing]
Forall2_dep_cons [in MetaRocq.Utils.All_Forall]
Forall2_dep_nil [in MetaRocq.Utils.All_Forall]
Forall3_cons [in MetaRocq.Utils.All_Forall]
Forall3_nil [in MetaRocq.Utils.All_Forall]
fot_view_other [in MetaRocq.Erasure.Typed.Erasure]
fot_view_sort [in MetaRocq.Erasure.Typed.Erasure]
fot_view_prod [in MetaRocq.Erasure.Typed.Erasure]
fo_None [in MetaRocq.Utils.MROption]
fo_Some [in MetaRocq.Utils.MROption]
fresh_globals_cons [in MetaRocq.Erasure.Typed.ExAst]
fresh_globals_empty [in MetaRocq.Erasure.Typed.ExAst]
fuel [in MetaRocq.Utils.MRUtils]



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)