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)

D (definition)

d [in MetaCoq.Examples.demo]
dapp_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dapp_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dcase_c [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dcase_preturn [in MetaCoq.PCUIC.Syntax.PCUICPosition]
debug_term [in MetaCoq.Translations.param_binary]
debug_term [in MetaCoq.Translations.standard_model]
debug_term [in MetaCoq.Translations.param_original]
DeclarationTyping.Forall_decls_typing [in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.isType [in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.type_local_decl [in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.wf_local_rel [in MetaCoq.Template.EnvironmentTyping]
declared [in MetaCoq.Template.common.uGraph]
declared_cstr_levels [in MetaCoq.Template.Universes]
declared_kn [in MetaCoq.Erasure.ErasureFunction]
declared_projection [in MetaCoq.Erasure.EGlobalEnv]
declared_constructor [in MetaCoq.Erasure.EGlobalEnv]
declared_inductive [in MetaCoq.Erasure.EGlobalEnv]
declared_minductive [in MetaCoq.Erasure.EGlobalEnv]
declared_constant [in MetaCoq.Erasure.EGlobalEnv]
decls_prefix [in MetaCoq.Erasure.ErasureFunction]
decl_size [in MetaCoq.Examples.tauto]
decl_size [in MetaCoq.PCUIC.utils.PCUICSize]
decl_depth_gen [in MetaCoq.PCUIC.Syntax.PCUICDepth]
decompose_prod_n_assum [in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum [in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod [in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app [in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec [in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_lam [in MetaCoq.Erasure.EPretty]
decompose_stack_at [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_app [in MetaCoq.Erasure.EAstUtils]
decompose_app_rec [in MetaCoq.Erasure.EAstUtils]
decompose_cstr_concl [in MetaCoq.SafeChecker.PCUICSafeChecker]
decompose_lam [in MetaCoq.Template.Pretty]
decompose_lam_n_assum [in MetaCoq.Template.AstUtils]
decompose_prod_n_assum [in MetaCoq.Template.AstUtils]
decompose_prod_assum [in MetaCoq.Template.AstUtils]
decompose_prod [in MetaCoq.Template.AstUtils]
decompose_app [in MetaCoq.Template.AstUtils]
decompose_lam [in MetaCoq.PCUIC.utils.PCUICPretty]
decomp_step [in MetaCoq.Examples.tauto]
default_term [in MetaCoq.Translations.param_binary]
default_fuel [in MetaCoq.Template.Checker]
default_term [in MetaCoq.Translations.standard_model]
default_wcbv_flags [in MetaCoq.Erasure.EWcbvEval]
default_term [in MetaCoq.Translations.param_original]
default_relevance [in MetaCoq.Template.AstUtils]
default_sort_family [in MetaCoq.Template.AstUtils]
def_sig [in MetaCoq.PCUIC.Syntax.PCUICPosition]
def_size [in MetaCoq.Examples.tauto]
def_size [in MetaCoq.PCUIC.utils.PCUICSize]
def_depth_gen [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth [in MetaCoq.PCUIC.Syntax.PCUICDepth]
destArity [in MetaCoq.Template.Ast]
destArity [in MetaCoq.PCUIC.PCUICAst]
destInd [in MetaCoq.Template.Typing]
destInd [in MetaCoq.PCUIC.PCUICTyping]
destInd [in MetaCoq.Template.AstUtils]
diamond [in MetaCoq.PCUIC.PCUICConfluence]
dirpath [in MetaCoq.Template.Kernames]
disable_projections_env_flag [in MetaCoq.Erasure.EInlineProjections]
disable_projections_term_flags [in MetaCoq.Erasure.EInlineProjections]
disable_prop_cases [in MetaCoq.Erasure.EInlineProjections]
disable_prop_cases [in MetaCoq.Erasure.EWcbvEval]
discr_expanded_head [in MetaCoq.Erasure.EEtaExpandedFix]
discr_construct0_cofix [in MetaCoq.PCUIC.Syntax.PCUICViews]
discr_construct_cofix [in MetaCoq.PCUIC.Syntax.PCUICViews]
discr_construct0_cofix [in MetaCoq.SafeChecker.PCUICSafeReduce]
discr_construct_cofix [in MetaCoq.SafeChecker.PCUICSafeReduce]
discr_construct [in MetaCoq.SafeChecker.PCUICSafeReduce]
discr_construct [in MetaCoq.Erasure.EEtaExpanded]
discr_prod_letin [in MetaCoq.SafeChecker.PCUICSafeChecker]
dlam_tm [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlam_ty [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlet_in [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlet_ty [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlet_bd [in MetaCoq.PCUIC.Syntax.PCUICPosition]
do_check_ind_sorts [in MetaCoq.SafeChecker.PCUICSafeChecker]
dpath_forall' [in MetaCoq.Translations.MiniHoTT]
dpath_forall_constant [in MetaCoq.Translations.MiniHoTT]
dpath_forall [in MetaCoq.Translations.MiniHoTT]
dpath_paths2 [in MetaCoq.Translations.MiniHoTT]
dpath_path_lFFr [in MetaCoq.Translations.MiniHoTT]
dpath_path_FFlr [in MetaCoq.Translations.MiniHoTT]
dpath_path_FlFr [in MetaCoq.Translations.MiniHoTT]
dpath_path_Fr [in MetaCoq.Translations.MiniHoTT]
dpath_path_Fl [in MetaCoq.Translations.MiniHoTT]
dpath_path_lr [in MetaCoq.Translations.MiniHoTT]
dpath_path_r [in MetaCoq.Translations.MiniHoTT]
dpath_path_l [in MetaCoq.Translations.MiniHoTT]
dpath_forall' [in MetaCoq.Translations.MiniHoTT_paths]
dpath_forall_constant [in MetaCoq.Translations.MiniHoTT_paths]
dpath_forall [in MetaCoq.Translations.MiniHoTT_paths]
dpath_paths2 [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_lFFr [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_FFlr [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_FlFr [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_Fr [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_Fl [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_lr [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_r [in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_l [in MetaCoq.Translations.MiniHoTT_paths]
dprod_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dprod_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dproj_c [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dummy_branch [in MetaCoq.Template.Typing]
dummy_branch [in MetaCoq.PCUIC.utils.PCUICOnOne]
dummy_decl [in MetaCoq.PCUIC.TemplateToPCUIC]


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)