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)

C (definition)

cancelL [in MetaCoq.Translations.MiniHoTT]
cancelL [in MetaCoq.Translations.MiniHoTT_paths]
cancelL_equiv [in MetaCoq.Translations.MiniHoTT]
cancelL_isequiv [in MetaCoq.Translations.MiniHoTT]
cancelL_equiv [in MetaCoq.Translations.MiniHoTT_paths]
cancelL_isequiv [in MetaCoq.Translations.MiniHoTT_paths]
cancelR [in MetaCoq.Translations.MiniHoTT]
cancelR [in MetaCoq.Translations.MiniHoTT_paths]
cancelR_equiv [in MetaCoq.Translations.MiniHoTT]
cancelR_isequiv [in MetaCoq.Translations.MiniHoTT]
cancelR_equiv [in MetaCoq.Translations.MiniHoTT_paths]
cancelR_isequiv [in MetaCoq.Translations.MiniHoTT_paths]
cancel2L [in MetaCoq.Translations.MiniHoTT]
cancel2L [in MetaCoq.Translations.MiniHoTT_paths]
cancel2R [in MetaCoq.Translations.MiniHoTT]
cancel2R [in MetaCoq.Translations.MiniHoTT_paths]
canonical_abstract_env_ext_impl [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
can_val_Prop [in MetaCoq.Examples.tauto]
can_val [in MetaCoq.Examples.tauto]
CaseBrsProp [in MetaCoq.PCUIC.Syntax.PCUICInduction]
CaseBrsProp [in MetaCoq.PCUIC.Syntax.PCUICDepth]
CaseBrsProp_depth [in MetaCoq.PCUIC.Syntax.PCUICDepth]
CasePredProp [in MetaCoq.PCUIC.Syntax.PCUICInduction]
CasePredProp [in MetaCoq.PCUIC.Syntax.PCUICDepth]
CasePredProp_depth [in MetaCoq.PCUIC.Syntax.PCUICDepth]
case_branch_type [in MetaCoq.Template.Ast]
case_branch_type_gen [in MetaCoq.Template.Ast]
case_branches_contexts [in MetaCoq.Template.Ast]
case_branches_contexts_gen [in MetaCoq.Template.Ast]
case_branch_context [in MetaCoq.Template.Ast]
case_branch_context_gen [in MetaCoq.Template.Ast]
case_predicate_context [in MetaCoq.Template.Ast]
case_predicate_context_gen [in MetaCoq.Template.Ast]
case_branch_context_nopars [in MetaCoq.PCUIC.PCUICInductiveInversion]
case_branch_type [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_type_gen [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branches_contexts [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branches_contexts_gen [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_context_gen [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_predicate_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_predicate_context_gen [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_predicate_context' [in MetaCoq.PCUIC.PCUICCasesContexts]
cc_viewc [in MetaCoq.SafeChecker.PCUICSafeReduce]
cc0_viewc [in MetaCoq.SafeChecker.PCUICSafeReduce]
cdecl_Type [in MetaCoq.Examples.tauto]
cf' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
check [in MetaCoq.Template.Checker]
check [in MetaCoq.SafeChecker.PCUICTypeChecker]
checkb_constructors_smaller [in MetaCoq.SafeChecker.PCUICSafeChecker]
checking_size_pos [in MetaCoq.PCUIC.Bidirectional.BDTyping]
checking_size [in MetaCoq.PCUIC.Bidirectional.BDTyping]
check_conv_pb_relb_correct [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
check_wf_eta [in MetaCoq.Template.TemplateCheckWf]
check_wf [in MetaCoq.Template.TemplateCheckWf]
check_def [in MetaCoq.Template.TemplateCheckWf]
check_one_cofix [in MetaCoq.Template.Typing]
check_one_fix [in MetaCoq.Template.Typing]
check_recursivity_kind [in MetaCoq.Template.Typing]
check_inh [in MetaCoq.Examples.typing_correctness]
check_eqb_universe [in MetaCoq.Template.common.uGraph]
check_leqb_universe [in MetaCoq.Template.common.uGraph]
check_constraints [in MetaCoq.Template.common.uGraph]
check_gc_constraints [in MetaCoq.Template.common.uGraph]
check_gc_constraint [in MetaCoq.Template.common.uGraph]
check_eqb_levelalg [in MetaCoq.Template.common.uGraph]
check_leqb_levelalg [in MetaCoq.Template.common.uGraph]
check_wf_declarations [in MetaCoq.Template.Checker]
check_fresh [in MetaCoq.Template.Checker]
check_wf_decl [in MetaCoq.Template.Checker]
check_wf_judgement [in MetaCoq.Template.Checker]
check_wf_type [in MetaCoq.Template.Checker]
check_consistent_constraints [in MetaCoq.Template.Checker]
check_conv [in MetaCoq.Template.Checker]
check_conv_leq [in MetaCoq.Template.Checker]
check_conv_gen [in MetaCoq.Template.Checker]
check_one_cofix [in MetaCoq.PCUIC.PCUICTyping]
check_one_fix [in MetaCoq.PCUIC.PCUICTyping]
check_recursivity_kind [in MetaCoq.PCUIC.PCUICTyping]
check_eq_nat [in MetaCoq.Template.monad_utils]
check_eq_true [in MetaCoq.Template.monad_utils]
check_dec [in MetaCoq.Template.monad_utils]
check_type_wf_env_fast [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_env_bool_spec2 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_env_bool_spec [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_type_wf_env_bool [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_ext [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_env [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_decls [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_univs [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_decl [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_one_ind_body [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_ind_types [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_indices [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_projections [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_projections_cs [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_projection [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_projections_type [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_constructors [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_cstr_variance [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_variance [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_local [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_positive_cstr [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_positive_cstr_arg [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_constructors_univs [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_constructor [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_constructor_spec [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_conv_args [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_leq_terms [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_compare_context [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_eq_decl [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_eq_term [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_type_local_ctx [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_context_wf_env [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_type_wf_env [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_env_ext_prop [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_udecl [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_fresh [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_judgement [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_wf_type [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_eq_true_lazy [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_inh [in MetaCoq.Examples.metacoq_tour_prelude]
check_isType [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_mfix_bodies [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_mfix_types [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_branches [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_is_allowed_elimination [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_consistent_instance [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_pb_terms [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_inst [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_alpha_ws_cumul_ctx [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_ctx [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_pb_decl [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_context_rel [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_context [in MetaCoq.SafeChecker.PCUICTypeChecker]
chop [in MetaCoq.Template.utils.MCList]
closedn [in MetaCoq.Template.Ast]
closedn [in MetaCoq.PCUIC.PCUICAst]
closedn [in MetaCoq.Erasure.ELiftSubst]
closedn_stack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_stack_entry [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_branches_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_predicate_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_context_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_mfix_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedu [in MetaCoq.Template.Ast]
closedu [in MetaCoq.PCUIC.PCUICAst]
closedu_instance [in MetaCoq.Template.Universes]
closedu_universe [in MetaCoq.Template.Universes]
closedu_universe_levels [in MetaCoq.Template.Universes]
closedu_level_expr [in MetaCoq.Template.Universes]
closedu_level [in MetaCoq.Template.Universes]
closedu_cstrs [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_cstr [in MetaCoq.PCUIC.PCUICInductiveInversion]
closed_red_red [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_red [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_red1_red1 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_red1 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_red_red [in MetaCoq.PCUIC.PCUICConvCumInversion]
closed_eprogram_env [in MetaCoq.Erasure.EProgram]
closed_eprogram [in MetaCoq.Erasure.EProgram]
closed_env [in MetaCoq.Erasure.EGlobalEnv]
closed_decl [in MetaCoq.Erasure.EGlobalEnv]
closed_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
closed_subst [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
closed_inductive_decl [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_constructor_body [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_red1_ctx [in MetaCoq.PCUIC.PCUICSR]
closed_red1_ind' [in MetaCoq.PCUIC.PCUICSR]
clos_sym [in MetaCoq.Template.utils.MCRelations]
clos_rt_monotone [in MetaCoq.Template.utils.MCRelations]
clos_rt_ctx_t_monotone [in MetaCoq.PCUIC.PCUICConfluence]
cod [in MetaCoq.Erasure.ErasureFunction]
coe [in MetaCoq.Translations.times_bool_fun2]
cofix_subst [in MetaCoq.Template.Typing]
cofix_subst [in MetaCoq.PCUIC.Syntax.PCUICCases]
cofix_guard [in MetaCoq.PCUIC.PCUICTyping]
cofix_subst [in MetaCoq.Erasure.EGlobalEnv]
cofix_guard_rename [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_inst [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_nl [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_context_cumulativity [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_extends [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_subst_instance [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_eq_term [in MetaCoq.PCUIC.PCUICGuardCondition]
cofix_guard_red1 [in MetaCoq.PCUIC.PCUICGuardCondition]
combine' [in MetaCoq.Translations.times_bool_fun]
Common_kn [in MetaCoq.Template.TemplateMonad.Core]
commutes [in MetaCoq.Template.utils.MCRelations]
compare [in MetaCoq.Template.utils.ByteCompare]
compare_cont [in MetaCoq.Template.utils.MCCompare]
compare_universe [in MetaCoq.Template.Universes]
compare_term [in MetaCoq.Template.TermEquality]
compare_context [in MetaCoq.PCUIC.PCUICEquality]
compare_decl [in MetaCoq.PCUIC.PCUICEquality]
compare_opt_term [in MetaCoq.PCUIC.PCUICEquality]
compare_term [in MetaCoq.PCUIC.PCUICEquality]
compare_term_napp [in MetaCoq.PCUIC.PCUICEquality]
compare_ident [in MetaCoq.Template.Kernames]
compare_context [in MetaCoq.PCUIC.PCUICContextConversion]
compare_global_instance_proper [in MetaCoq.SafeChecker.PCUICEqualityDec]
compare_global_instance [in MetaCoq.SafeChecker.PCUICEqualityDec]
compare_universe_instance_variance [in MetaCoq.SafeChecker.PCUICEqualityDec]
compare_universe_instance [in MetaCoq.SafeChecker.PCUICEqualityDec]
compare_universe_variance [in MetaCoq.SafeChecker.PCUICEqualityDec]
comparison_trans [in MetaCoq.Template.utils.MCCompare]
composeD [in MetaCoq.Translations.MiniHoTT]
composeD [in MetaCoq.Translations.MiniHoTT_paths]
Computational [in MetaCoq.PCUIC.PCUICElimination]
computational_type [in MetaCoq.Erasure.Extract]
computational_ind [in MetaCoq.Erasure.Extract]
concat [in MetaCoq.Translations.MiniHoTT]
concat [in MetaCoq.Translations.MiniHoTT_paths]
concat_whisker [in MetaCoq.Translations.MiniHoTT]
concat_concat2 [in MetaCoq.Translations.MiniHoTT]
concat_AT [in MetaCoq.Translations.MiniHoTT]
concat_p_A1p [in MetaCoq.Translations.MiniHoTT]
concat_pp_A1 [in MetaCoq.Translations.MiniHoTT]
concat_A1_pp [in MetaCoq.Translations.MiniHoTT]
concat_pA1_p [in MetaCoq.Translations.MiniHoTT]
concat_pp_A1p [in MetaCoq.Translations.MiniHoTT]
concat_pA1_pp [in MetaCoq.Translations.MiniHoTT]
concat_A_pp [in MetaCoq.Translations.MiniHoTT]
concat_pA_p [in MetaCoq.Translations.MiniHoTT]
concat_pA_pp [in MetaCoq.Translations.MiniHoTT]
concat_pA1 [in MetaCoq.Translations.MiniHoTT]
concat_A1p [in MetaCoq.Translations.MiniHoTT]
concat_Ap [in MetaCoq.Translations.MiniHoTT]
concat_pV_p [in MetaCoq.Translations.MiniHoTT]
concat_pp_V [in MetaCoq.Translations.MiniHoTT]
concat_p_Vp [in MetaCoq.Translations.MiniHoTT]
concat_V_pp [in MetaCoq.Translations.MiniHoTT]
concat_Vp [in MetaCoq.Translations.MiniHoTT]
concat_pV [in MetaCoq.Translations.MiniHoTT]
concat_pp_p [in MetaCoq.Translations.MiniHoTT]
concat_p_pp [in MetaCoq.Translations.MiniHoTT]
concat_1p [in MetaCoq.Translations.MiniHoTT]
concat_p1 [in MetaCoq.Translations.MiniHoTT]
concat_whisker [in MetaCoq.Translations.MiniHoTT_paths]
concat_concat2 [in MetaCoq.Translations.MiniHoTT_paths]
concat_AT [in MetaCoq.Translations.MiniHoTT_paths]
concat_p_A1p [in MetaCoq.Translations.MiniHoTT_paths]
concat_pp_A1 [in MetaCoq.Translations.MiniHoTT_paths]
concat_A1_pp [in MetaCoq.Translations.MiniHoTT_paths]
concat_pA1_p [in MetaCoq.Translations.MiniHoTT_paths]
concat_pp_A1p [in MetaCoq.Translations.MiniHoTT_paths]
concat_pA1_pp [in MetaCoq.Translations.MiniHoTT_paths]
concat_A_pp [in MetaCoq.Translations.MiniHoTT_paths]
concat_pA_p [in MetaCoq.Translations.MiniHoTT_paths]
concat_pA_pp [in MetaCoq.Translations.MiniHoTT_paths]
concat_pA1 [in MetaCoq.Translations.MiniHoTT_paths]
concat_A1p [in MetaCoq.Translations.MiniHoTT_paths]
concat_Ap [in MetaCoq.Translations.MiniHoTT_paths]
concat_pV_p [in MetaCoq.Translations.MiniHoTT_paths]
concat_pp_V [in MetaCoq.Translations.MiniHoTT_paths]
concat_p_Vp [in MetaCoq.Translations.MiniHoTT_paths]
concat_V_pp [in MetaCoq.Translations.MiniHoTT_paths]
concat_Vp [in MetaCoq.Translations.MiniHoTT_paths]
concat_pV [in MetaCoq.Translations.MiniHoTT_paths]
concat_pp_p [in MetaCoq.Translations.MiniHoTT_paths]
concat_p_pp [in MetaCoq.Translations.MiniHoTT_paths]
concat_1p [in MetaCoq.Translations.MiniHoTT_paths]
concat_p1 [in MetaCoq.Translations.MiniHoTT_paths]
concat2 [in MetaCoq.Translations.MiniHoTT]
concat2 [in MetaCoq.Translations.MiniHoTT_paths]
concat2_1p [in MetaCoq.Translations.MiniHoTT]
concat2_p1 [in MetaCoq.Translations.MiniHoTT]
concat2_1p [in MetaCoq.Translations.MiniHoTT_paths]
concat2_p1 [in MetaCoq.Translations.MiniHoTT_paths]
confluent [in MetaCoq.PCUIC.PCUICConfluence]
conj_impl [in MetaCoq.PCUIC.PCUICSR]
consistent [in MetaCoq.Template.Universes]
consistent_extension_on [in MetaCoq.Template.Universes]
const [in MetaCoq.Translations.MiniHoTT]
const [in MetaCoq.Translations.MiniHoTT_paths]
ConstraintSetsUIP.cs_tree_rect [in MetaCoq.Template.Reflect]
ConstraintSetsUIP.cs_tree_eqb [in MetaCoq.Template.Reflect]
ConstraintSetsUIP.eqb_ConstraintSet [in MetaCoq.Template.Reflect]
constraints_of_udecl [in MetaCoq.Template.Universes]
ConstraintType.compare [in MetaCoq.Template.Universes]
ConstraintType.eq [in MetaCoq.Template.Universes]
ConstraintType.eq_equiv [in MetaCoq.Template.Universes]
ConstraintType.Le0 [in MetaCoq.Template.Universes]
ConstraintType.lt [in MetaCoq.Template.Universes]
ConstraintType.Lt [in MetaCoq.Template.Universes]
ConstraintType.t [in MetaCoq.Template.Universes]
constraint_lt_ind_dep [in MetaCoq.Template.Reflect]
constraint_type_lt_ind_dep [in MetaCoq.Template.Reflect]
constructor [in MetaCoq.Examples.constructor_tac]
constructors_as_blocks_transformation [in MetaCoq.Erasure.ETransform]
constructor_isprop_pars_decl [in MetaCoq.Erasure.EGlobalEnv]
construct_cofix_discr [in MetaCoq.PCUIC.Syntax.PCUICViews]
construct_viewc [in MetaCoq.SafeChecker.PCUICSafeReduce]
construct_viewc [in MetaCoq.Erasure.EEtaExpanded]
cons_decl [in MetaCoq.PCUIC.PCUICReduction]
context [in MetaCoq.Erasure.EAst]
ContextSet.constraints [in MetaCoq.Template.Universes]
ContextSet.empty [in MetaCoq.Template.Universes]
ContextSet.equal [in MetaCoq.Template.Universes]
ContextSet.inter [in MetaCoq.Template.Universes]
ContextSet.inter_spec [in MetaCoq.Template.Universes]
ContextSet.is_empty [in MetaCoq.Template.Universes]
ContextSet.levels [in MetaCoq.Template.Universes]
ContextSet.subset [in MetaCoq.Template.Universes]
ContextSet.t [in MetaCoq.Template.Universes]
ContextSet.union [in MetaCoq.Template.Universes]
ContextSet.union_spec [in MetaCoq.Template.Universes]
context_env_clos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_clos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_position [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_hole_choice [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_hole_context [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_choice_term [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_choice [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_size [in MetaCoq.Examples.tauto]
context_size [in MetaCoq.PCUIC.utils.PCUICSize]
context_depth_gen [in MetaCoq.PCUIC.Syntax.PCUICDepth]
contr [in MetaCoq.Translations.times_bool_fun2]
contr_equiv' [in MetaCoq.Translations.MiniHoTT]
contr_dom_equiv [in MetaCoq.Translations.MiniHoTT]
contr_equiv' [in MetaCoq.Translations.MiniHoTT_paths]
contr_dom_equiv [in MetaCoq.Translations.MiniHoTT_paths]
contr_retract_α [in MetaCoq.Translations.times_bool_fun2]
contr_retractα [in MetaCoq.Translations.times_bool_fun2]
contr_isequivα [in MetaCoq.Translations.times_bool_fun2]
contr_retract [in MetaCoq.Translations.times_bool_fun2]
Conversion.cumul_ctx_rel [in MetaCoq.Template.EnvironmentTyping]
Conversion.cumul_pb_context [in MetaCoq.Template.EnvironmentTyping]
Conversion.cumul_pb_decls [in MetaCoq.Template.EnvironmentTyping]
convert [in MetaCoq.SafeChecker.PCUICTypeChecker]
convert_leq [in MetaCoq.Template.Checker]
convSpec [in MetaCoq.PCUIC.PCUICCumulativitySpec]
conv_ctx_refl' [in MetaCoq.PCUIC.PCUICCumulativity]
conv_decls_prop [in MetaCoq.PCUIC.PCUICCumulProp]
conv_cum [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
conv_cum_napp [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_cum [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_ctx_refl' [in MetaCoq.PCUIC.PCUICCumulativitySpec]
conv_pb_relb [in MetaCoq.SafeChecker.PCUICEqualityDec]
conv_pb_relb_gen [in MetaCoq.SafeChecker.PCUICEqualityDec]
conv_pb_relb_gen_proper [in MetaCoq.SafeChecker.PCUICTypeChecker]
cored' [in MetaCoq.PCUIC.PCUICSN]
cstr_arity [in MetaCoq.PCUIC.PCUICWcbvEval]
cstr_branch_context [in MetaCoq.Template.Ast]
cstr_branch_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
cstr_arity [in MetaCoq.Erasure.EAst]
cstr_arity [in MetaCoq.Template.WcbvEval]
csubst [in MetaCoq.PCUIC.PCUICCSubst]
csubst [in MetaCoq.Template.WcbvEval]
csubst [in MetaCoq.Erasure.ECSubst]
cs_equal [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctxmap [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx_inst_size [in MetaCoq.Template.Typing]
ctx_inst_size [in MetaCoq.PCUIC.PCUICTyping]
ctx_inst_sub [in MetaCoq.PCUIC.PCUICSpine]
cumulSpec [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul_ctx_refl' [in MetaCoq.PCUIC.PCUICCumulativity]
cumul_ctx_refl' [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul_Construct_univ [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul_Ind_univ [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul_predicate [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul_decl [in MetaCoq.SafeChecker.PCUICSafeChecker]
cunfold_cofix [in MetaCoq.PCUIC.PCUICWcbvEval]
cunfold_fix [in MetaCoq.PCUIC.PCUICWcbvEval]
cunfold_cofix [in MetaCoq.Template.WcbvEval]
cunfold_fix [in MetaCoq.Template.WcbvEval]
cunfold_cofix [in MetaCoq.Erasure.EGlobalEnv]
cunfold_fix [in MetaCoq.Erasure.EGlobalEnv]
cuniv_of_product [in MetaCoq.Template.Universes]
cuniv_sup [in MetaCoq.Template.Universes]


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)