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

fail_nf [in MetaRocq.Template.TemplateMonad.Core]
fake_params [in MetaRocq.PCUIC.PCUICNormal]
fake_guard_impl [in MetaRocq.Erasure.Typed.Erasure]
fake_params [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fake_guard_impl [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
False_mib [in MetaRocq.PCUIC.PCUICConsistency]
False_oib [in MetaRocq.PCUIC.PCUICConsistency]
Fast.strip [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_env [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_decl [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_inductive_decl [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_constant_decl [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_defs [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_brs [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_args [in MetaRocq.Erasure.ERemoveParams]
fill_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_branches_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_predicate_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_context_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_mfix_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_branch_context [in MetaRocq.PCUIC.PCUICReduction]
fill_list_context [in MetaRocq.PCUIC.PCUICReduction]
fill_context [in MetaRocq.PCUIC.PCUICReduction]
filter_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
final_wcbv_flags [in MetaRocq.ErasurePlugin.Erasure]
find_tag [in MetaRocq.Erasure.EReorderCstrs]
firstorder_spine_sind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_rec [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_ind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_rect [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_sind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_ind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_env [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_env' [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_ind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_mutind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_oneind [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_con [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_type [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_evalue_elim [in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_sind [in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_ind [in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_block_sind [in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder_evalue_block_ind [in MetaRocq.ErasurePlugin.ErasureCorrectness]
FixCoFix_sind [in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_rec [in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_ind [in MetaRocq.PCUIC.PCUICTyping]
FixCoFix_rect [in MetaRocq.PCUIC.PCUICTyping]
fix_context_alt [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_context_gen [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
fix_context [in MetaRocq.Template.Pretty]
fix_guard_rename [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_inst [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_context_cumulativity [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_extends [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_subst_instance [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_eq_term [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard_red1 [in MetaRocq.PCUIC.PCUICGuardCondition]
fix_guard [in MetaRocq.PCUIC.PCUICTyping]
fix_or_cofix [in MetaRocq.PCUIC.PCUICConversion]
fix_lambda_view_sind [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view_rec [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view_ind [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_view_rect [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_sind [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_rec [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_ind [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_lambda_app_view_rect [in MetaRocq.PCUIC.Syntax.PCUICViews]
fix_context [in MetaRocq.Template.Typing]
fix_subst [in MetaRocq.Template.Typing]
fix_decls [in MetaRocq.Template.Checker]
fix_env [in MetaRocq.Erasure.EWcbvEvalNamed]
fix_subst [in MetaRocq.PCUIC.Syntax.PCUICCases]
fix_kind_sind [in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind_rec [in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind_ind [in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_kind_rect [in MetaRocq.SafeChecker.PCUICSafeConversion]
fix_subst [in MetaRocq.Erasure.EGlobalEnv]
flags_after_projs [in MetaRocq.Erasure.EInlineProjections]
flag_of_type [in MetaRocq.Erasure.Typed.Erasure]
flag_of_type_impl [in MetaRocq.Erasure.Typed.TypeAnnotations]
float64_to_model [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
float64_model [in MetaRocq.Common.BasicAst]
float64_from_model [in MetaRocq.TemplatePCUIC.PCUICToTemplate]
FMapAVL.Decide.Raw.bst_dec [in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.gt_tree_dec [in MetaRocq.Utils.MRFSets]
FMapAVL.Decide.Raw.lt_tree_dec [in MetaRocq.Utils.MRFSets]
fold_left_i [in MetaRocq.Utils.MRList]
fold_left_i_aux [in MetaRocq.Utils.MRList]
fold_termM [in MetaRocq.Template.AstUtils]
fold_term [in MetaRocq.Template.AstUtils]
fold_term_with_bindersM [in MetaRocq.Template.AstUtils]
fold_branch_with_bindersM [in MetaRocq.Template.AstUtils]
fold_predicate_with_bindersM [in MetaRocq.Template.AstUtils]
fold_term_with_binders [in MetaRocq.Template.AstUtils]
fold_branch_with_binders [in MetaRocq.Template.AstUtils]
fold_predicate_with_binders [in MetaRocq.Template.AstUtils]
fold_lefti [in MetaRocq.Erasure.Typed.Optimize]
fold_context_k_defs [in MetaRocq.Template.EtaExpand]
fold_context [in MetaRocq.Common.BasicAst]
fold_context_In [in MetaRocq.Common.BasicAst]
fold_context_k [in MetaRocq.Common.BasicAst]
fold_fix_context_alt [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_wf [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_prim [in MetaRocq.Erasure.EPrimitive]
foo [in MetaRocq.Examples.metarocq_tour]
forallbi [in MetaRocq.Erasure.Typed.Optimize]
forallbi [in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallb_InP [in MetaRocq.Utils.MRList]
forallb2 [in MetaRocq.Utils.All_Forall]
forallb2_proper [in MetaRocq.SafeChecker.PCUICSafeConversion]
forallb3 [in MetaRocq.Utils.All_Forall]
Forall_typing_spine_sind [in MetaRocq.Template.Typing]
Forall_typing_spine_rec [in MetaRocq.Template.Typing]
Forall_typing_spine_ind [in MetaRocq.Template.Typing]
Forall_typing_spine_rect [in MetaRocq.Template.Typing]
Forall2_dep_rec [in MetaRocq.Utils.All_Forall]
Forall2_dep_rect [in MetaRocq.Utils.All_Forall]
Forall2_rec [in MetaRocq.Utils.All_Forall]
Forall2_rect [in MetaRocq.Utils.All_Forall]
Forall2_dep_sind [in MetaRocq.Utils.All_Forall]
Forall2_dep_ind [in MetaRocq.Utils.All_Forall]
Forall3_sind [in MetaRocq.Utils.All_Forall]
Forall3_ind [in MetaRocq.Utils.All_Forall]
forget_inlining_info_transformation [in MetaRocq.Erasure.EInlining]
forget_inlining_info [in MetaRocq.Erasure.EInlining]
forget_types [in MetaRocq.Template.AstUtils]
forget_types [in MetaRocq.Common.BasicAst]
form_sind [in MetaRocq.Examples.tauto]
form_rec [in MetaRocq.Examples.tauto]
form_ind [in MetaRocq.Examples.tauto]
form_rect [in MetaRocq.Examples.tauto]
foroptb [in MetaRocq.Utils.MROption]
foroptb2 [in MetaRocq.Utils.MROption]
ForOption_sind [in MetaRocq.Utils.MROption]
ForOption_ind [in MetaRocq.Utils.MROption]
fot_viewc [in MetaRocq.Erasure.Typed.Erasure]
fot_view_sind [in MetaRocq.Erasure.Typed.Erasure]
fot_view_rec [in MetaRocq.Erasure.Typed.Erasure]
fot_view_ind [in MetaRocq.Erasure.Typed.Erasure]
fot_view_rect [in MetaRocq.Erasure.Typed.Erasure]
fo_evalue_map [in MetaRocq.ErasurePlugin.ErasureCorrectness]
fo_evalue [in MetaRocq.ErasurePlugin.ErasureCorrectness]
fresh [in MetaRocq.Template.Checker]
fresh [in MetaRocq.Erasure.EWcbvEvalNamed]
fresh_universe [in MetaRocq.Common.Universes]
fresh_level [in MetaRocq.Common.Universes]
fresh_names [in MetaRocq.Template.Pretty]
fresh_name [in MetaRocq.Template.Pretty]
fresh_id_from [in MetaRocq.Template.Pretty]
fresh_globals_sind [in MetaRocq.Erasure.Typed.ExAst]
fresh_globals_ind [in MetaRocq.Erasure.Typed.ExAst]
fresh_global [in MetaRocq.Erasure.Typed.ExAst]
fresh_names [in MetaRocq.PCUIC.utils.PCUICPretty]
fresh_name [in MetaRocq.PCUIC.utils.PCUICPretty]
fresh_id_from [in MetaRocq.PCUIC.utils.PCUICPretty]
fresh_evar_id [in MetaRocq.Common.BasicAst]
fresh_name [in MetaRocq.Erasure.EPretty]
fresh_id_from [in MetaRocq.Erasure.EPretty]
fresh_global [in MetaRocq.Erasure.EGlobalEnv]
from_oib [in MetaRocq.Erasure.Typed.CertifyingEta]
FSets.WFactsExtra_fun.Equiv_alt [in MetaRocq.Utils.MRFSets]
fst_ctx [in MetaRocq.PCUIC.utils.PCUICAstUtils]
fst_eq [in MetaRocq.Utils.MRProd]
Funtm [in MetaRocq.Examples.demo]
Funtp [in MetaRocq.Examples.demo]
Funtp2 [in MetaRocq.Examples.demo]


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)