| 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) |
C (definition)
canonical_abstract_env_impl [in MetaRocq.SafeChecker.PCUICWfEnvImpl]can_val_Prop [in MetaRocq.Examples.tauto]
can_val [in MetaRocq.Examples.tauto]
can_have_args [in MetaRocq.Erasure.Typed.ExAst]
CaseBrsProp [in MetaRocq.PCUIC.Syntax.PCUICInduction]
CaseBrsProp [in MetaRocq.PCUIC.Syntax.PCUICDepth]
CaseBrsProp_depth [in MetaRocq.PCUIC.Syntax.PCUICDepth]
CasePredProp [in MetaRocq.PCUIC.Syntax.PCUICInduction]
CasePredProp [in MetaRocq.PCUIC.Syntax.PCUICDepth]
CasePredProp_depth [in MetaRocq.PCUIC.Syntax.PCUICDepth]
case_branch_context_nopars [in MetaRocq.PCUIC.PCUICInductiveInversion]
case_predicate_context' [in MetaRocq.PCUIC.PCUICCasesContexts]
case_branch_type [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_type_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branches_contexts [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branches_contexts_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_type [in MetaRocq.Template.Ast]
case_branch_type_gen [in MetaRocq.Template.Ast]
case_branches_contexts [in MetaRocq.Template.Ast]
case_branches_contexts_gen [in MetaRocq.Template.Ast]
case_branch_context [in MetaRocq.Template.Ast]
case_branch_context_gen [in MetaRocq.Template.Ast]
case_predicate_context [in MetaRocq.Template.Ast]
case_predicate_context_gen [in MetaRocq.Template.Ast]
case_branch_type_subst [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_subst_gen [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_only [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_only_gen [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_context [in MetaRocq.PCUIC.PCUICCasesHelper]
cast_kind_sind [in MetaRocq.Common.BasicAst]
cast_kind_rec [in MetaRocq.Common.BasicAst]
cast_kind_ind [in MetaRocq.Common.BasicAst]
cast_kind_rect [in MetaRocq.Common.BasicAst]
cc_viewc [in MetaRocq.SafeChecker.PCUICSafeReduce]
cc0_viewc [in MetaRocq.SafeChecker.PCUICSafeReduce]
cdecl_Type [in MetaRocq.Examples.tauto]
cf' [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
change_modpath [in MetaRocq.Erasure.Typed.Certifying]
char63_to_string [in MetaRocq.Utils.Show]
check [in MetaRocq.Template.Checker]
check [in MetaRocq.SafeChecker.PCUICTypeChecker]
checkb_constructors_smaller [in MetaRocq.SafeChecker.PCUICSafeChecker]
checking_size_pos [in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_size [in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_sind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_rec [in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_ind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_rect [in MetaRocq.PCUIC.Bidirectional.BDTyping]
check_wf_and_extract [in MetaRocq.Erasure.Typed.Extraction]
check_inh [in MetaRocq.Examples.typing_correctness]
check_one_cofix [in MetaRocq.PCUIC.PCUICTyping]
check_one_fix [in MetaRocq.PCUIC.PCUICTyping]
check_recursivity_kind [in MetaRocq.PCUIC.PCUICTyping]
check_cmpb_sort_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
check_cmpb_universe_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
check_oib_masks [in MetaRocq.Erasure.Typed.Optimize]
check_eq_nat [in MetaRocq.Utils.monad_utils]
check_eq_true [in MetaRocq.Utils.monad_utils]
check_dec [in MetaRocq.Utils.monad_utils]
check_type_wf_env_fast [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env_bool_spec2 [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env_bool_spec [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_type_wf_env_bool [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_ext [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_decls [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_univs [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_decl [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_one_ind_body [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_ind_types [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_indices [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projections [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projections_cs [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projection [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projections_type [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructors [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_cstr_variance [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_variance [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_local [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_positive_cstr [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_positive_cstr_arg [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructors_univs [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructor [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructor_spec [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_conv_args [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_leq_terms [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_compare_context [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_eq_decl [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_eq_term [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_type_local_ctx [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_context_wf_env [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_type_wf_env [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env_ext_prop [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_udecl [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_fresh [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_judgement [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_type [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_eq_true_lazy [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_eta [in MetaRocq.Template.TemplateCheckWf]
check_wf [in MetaRocq.Template.TemplateCheckWf]
check_def [in MetaRocq.Template.TemplateCheckWf]
check_one_cofix [in MetaRocq.Template.Typing]
check_one_fix [in MetaRocq.Template.Typing]
check_recursivity_kind [in MetaRocq.Template.Typing]
check_dearging_trans [in MetaRocq.ErasurePlugin.ETransform]
check_dearging_precond [in MetaRocq.ErasurePlugin.ETransform]
check_wf_declarations [in MetaRocq.Template.Checker]
check_fresh [in MetaRocq.Template.Checker]
check_wf_decl [in MetaRocq.Template.Checker]
check_wf_judgement [in MetaRocq.Template.Checker]
check_wf_type [in MetaRocq.Template.Checker]
check_consistent_constraints [in MetaRocq.Template.Checker]
check_conv [in MetaRocq.Template.Checker]
check_conv_leq [in MetaRocq.Template.Checker]
check_conv_gen [in MetaRocq.Template.Checker]
check_inh [in MetaRocq.Examples.metarocq_tour_prelude]
check_oib_masks_trans [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
check_eqb_sort_complete [in MetaRocq.Common.uGraph]
check_eqb_sort_spec' [in MetaRocq.Common.uGraph]
check_leqb_sort_complete [in MetaRocq.Common.uGraph]
check_leqb_sort_spec' [in MetaRocq.Common.uGraph]
check_constraints_complete [in MetaRocq.Common.uGraph]
check_constraints_spec [in MetaRocq.Common.uGraph]
check_gc_constraints_complete [in MetaRocq.Common.uGraph]
check_gc_constraint_complete [in MetaRocq.Common.uGraph]
check_eqb_universe_complete [in MetaRocq.Common.uGraph]
check_eqb_universe_spec' [in MetaRocq.Common.uGraph]
check_leqb_universe_complete [in MetaRocq.Common.uGraph]
check_leqb_universe_spec' [in MetaRocq.Common.uGraph]
check_eqb_sort_spec [in MetaRocq.Common.uGraph]
check_eqb_sort_refl [in MetaRocq.Common.uGraph]
check_eqb_sort [in MetaRocq.Common.uGraph]
check_leqb_sort [in MetaRocq.Common.uGraph]
check_gc_constraints_spec [in MetaRocq.Common.uGraph]
check_gc_constraint_spec [in MetaRocq.Common.uGraph]
check_constraints [in MetaRocq.Common.uGraph]
check_gc_constraints [in MetaRocq.Common.uGraph]
check_gc_constraint [in MetaRocq.Common.uGraph]
check_eqb_universe_spec [in MetaRocq.Common.uGraph]
check_eqb_universe [in MetaRocq.Common.uGraph]
check_leqb_universe_spec [in MetaRocq.Common.uGraph]
check_leqb_universe [in MetaRocq.Common.uGraph]
check_eqb_sort_gen [in MetaRocq.Common.uGraph]
check_leqb_sort_gen [in MetaRocq.Common.uGraph]
check_constraints_gen [in MetaRocq.Common.uGraph]
check_gc_constraints_gen [in MetaRocq.Common.uGraph]
check_gc_constraint_gen [in MetaRocq.Common.uGraph]
check_eqb_universe_gen [in MetaRocq.Common.uGraph]
check_leqb_universe_gen [in MetaRocq.Common.uGraph]
check_isType [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_primitive_typing [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_primitive_invariants [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_mfix_bodies [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_mfix_types [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_branches [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_is_allowed_elimination [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_consistent_instance [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_pb_terms [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_inst [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_alpha_ws_cumul_ctx [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_ctx [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_pb_decl [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_context_rel [in MetaRocq.SafeChecker.PCUICTypeChecker]
check_context [in MetaRocq.SafeChecker.PCUICTypeChecker]
choice_sind [in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_rec [in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_ind [in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_rect [in MetaRocq.PCUIC.Syntax.PCUICPosition]
chop [in MetaRocq.Utils.MRList]
clear_bit [in MetaRocq.Erasure.Typed.Optimize]
closedn [in MetaRocq.PCUIC.PCUICAst]
closedn [in MetaRocq.Template.Ast]
closedn [in MetaRocq.Erasure.ELiftSubst]
closedn_stack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_stack_entry [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_branches_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_predicate_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_context_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_mfix_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedu [in MetaRocq.PCUIC.PCUICAst]
closedu [in MetaRocq.Template.Ast]
closedu_instance [in MetaRocq.Common.Universes]
closedu_sort [in MetaRocq.Common.Universes]
closedu_universe [in MetaRocq.Common.Universes]
closedu_level_expr [in MetaRocq.Common.Universes]
closedu_level [in MetaRocq.Common.Universes]
closedu_cstrs [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_cstr [in MetaRocq.PCUIC.PCUICInductiveInversion]
closed_red1_ctx [in MetaRocq.PCUIC.PCUICSR]
closed_red1_ind' [in MetaRocq.PCUIC.PCUICSR]
closed_inductive_decl [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_inductive_body [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_constructor_body [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_red_red [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red1_red1 [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red1 [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
closed_subst [in MetaRocq.PCUIC.Syntax.PCUICInstDef]
closed_eprogram_env [in MetaRocq.Erasure.EProgram]
closed_eprogram [in MetaRocq.Erasure.EProgram]
closed_red_red [in MetaRocq.PCUIC.PCUICConvCumInversion]
closed_env [in MetaRocq.Erasure.EGlobalEnv]
closed_decl [in MetaRocq.Erasure.EGlobalEnv]
clos_refl_trans_ctx_1n_sind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_rec [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_ind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_rect [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_monotone [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_sind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_rec [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_ind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_rect [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_sind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_rec [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_ind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_rect [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_sind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_rec [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_ind [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_rect [in MetaRocq.PCUIC.PCUICConfluence]
clos_sym [in MetaRocq.Utils.MRRelations]
clos_rt_monotone [in MetaRocq.Utils.MRRelations]
cmp_ind_universes [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_gen [in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_dep [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance [in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_gen [in MetaRocq.Template.TermEquality]
cmp_opt_variance [in MetaRocq.Template.TermEquality]
cmp_universe_instance_variance [in MetaRocq.Template.TermEquality]
cmp_universe_variance [in MetaRocq.Template.TermEquality]
cmp_universe_instance [in MetaRocq.Template.TermEquality]
cod [in MetaRocq.Erasure.ErasureFunction]
cofix_guard_rename [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_inst [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_context_cumulativity [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_extends [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_subst_instance [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_eq_term [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_red1 [in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard [in MetaRocq.PCUIC.PCUICTyping]
cofix_subst [in MetaRocq.Template.Typing]
cofix_subst [in MetaRocq.PCUIC.Syntax.PCUICCases]
cofix_subst [in MetaRocq.Erasure.EGlobalEnv]
coinductive_to_inductive_transformation [in MetaRocq.ErasurePlugin.ETransform]
combine_valuations [in MetaRocq.Common.UniversesDec]
Common_kn [in MetaRocq.Template.TemplateMonad.Core]
common_prefix [in MetaRocq.Quotation.CommonUtils]
common_prefix_ls [in MetaRocq.Quotation.CommonUtils]
commutes [in MetaRocq.Utils.MRRelations]
compare [in MetaRocq.Utils.ByteCompare]
compare_context [in MetaRocq.PCUIC.PCUICEquality]
compare_decl [in MetaRocq.PCUIC.PCUICEquality]
compare_opt_term [in MetaRocq.PCUIC.PCUICEquality]
compare_term [in MetaRocq.PCUIC.PCUICEquality]
compare_term_napp [in MetaRocq.PCUIC.PCUICEquality]
compare_decls [in MetaRocq.PCUIC.PCUICEquality]
compare_cont [in MetaRocq.Utils.MRCompare]
compare_sort [in MetaRocq.Common.Universes]
compare_universe [in MetaRocq.Common.Universes]
compare_term [in MetaRocq.Template.TermEquality]
compare_global_instance_proper [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universe_instance_variance [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universe_instance [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universe_variance [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_context [in MetaRocq.PCUIC.PCUICContextConversion]
compare_ident [in MetaRocq.Common.Kernames]
compare_global_instance_correct [in MetaRocq.SafeChecker.PCUICSafeConversion]
comparison_trans [in MetaRocq.Utils.MRCompare]
compile_value_erase [in MetaRocq.Erasure.ErasureFunctionProperties]
compile_evalue_box [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_strip [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_value_box [in MetaRocq.ErasurePlugin.ErasureCorrectness]
complete_ctx_mask [in MetaRocq.Erasure.Typed.Optimize]
compose_transforms [in MetaRocq.Erasure.Typed.Transform]
Computational [in MetaRocq.PCUIC.PCUICElimination]
computational_type [in MetaRocq.Erasure.Extract]
computational_ind [in MetaRocq.Erasure.Extract]
compute_masks [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
compute_masks [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
concrete_sort [in MetaRocq.Common.Universes]
confluent [in MetaRocq.PCUIC.PCUICConfluence]
consistent [in MetaRocq.Common.Universes]
consistent_extension_on [in MetaRocq.Common.Universes]
consistent_extension_on_dec [in MetaRocq.Common.UniversesDec]
consistent_dec [in MetaRocq.Common.UniversesDec]
constansts_info [in MetaRocq.Erasure.Typed.CertifyingEta]
constants_inlining [in MetaRocq.Erasure.EInlining]
constant_body_annots [in MetaRocq.Erasure.Typed.Annotations]
constant_decls_deps [in MetaRocq.Erasure.ErasureFunction]
constant_entry_sind [in MetaRocq.PCUIC.PCUICAst]
constant_entry_rec [in MetaRocq.PCUIC.PCUICAst]
constant_entry_ind [in MetaRocq.PCUIC.PCUICAst]
constant_entry_rect [in MetaRocq.PCUIC.PCUICAst]
constant_entry_sind [in MetaRocq.Erasure.EAst]
constant_entry_rec [in MetaRocq.Erasure.EAst]
constant_entry_ind [in MetaRocq.Erasure.EAst]
constant_entry_rect [in MetaRocq.Erasure.EAst]
constant_entry_sind [in MetaRocq.Template.Ast]
constant_entry_rec [in MetaRocq.Template.Ast]
constant_entry_ind [in MetaRocq.Template.Ast]
constant_entry_rect [in MetaRocq.Template.Ast]
ConstraintSetsUIP.cs_tree_rect [in MetaRocq.Common.Reflect]
ConstraintSetsUIP.cs_tree_eqb [in MetaRocq.Common.Reflect]
ConstraintSetsUIP.eqb_ConstraintSet [in MetaRocq.Common.Reflect]
constraints_of_udecl [in MetaRocq.Common.Universes]
ConstraintType.compare [in MetaRocq.Common.Universes]
ConstraintType.eq [in MetaRocq.Common.Universes]
ConstraintType.eq_equiv [in MetaRocq.Common.Universes]
ConstraintType.Le0 [in MetaRocq.Common.Universes]
ConstraintType.lt [in MetaRocq.Common.Universes]
ConstraintType.Lt [in MetaRocq.Common.Universes]
ConstraintType.lt__sind [in MetaRocq.Common.Universes]
ConstraintType.lt__ind [in MetaRocq.Common.Universes]
ConstraintType.t [in MetaRocq.Common.Universes]
ConstraintType.t__sind [in MetaRocq.Common.Universes]
ConstraintType.t__rec [in MetaRocq.Common.Universes]
ConstraintType.t__ind [in MetaRocq.Common.Universes]
ConstraintType.t__rect [in MetaRocq.Common.Universes]
constraint_lt_ind_dep [in MetaRocq.Common.Reflect]
constraint_type_lt_ind_dep [in MetaRocq.Common.Reflect]
constructor [in MetaRocq.Examples.constructor_tac]
constructors_as_blocks_transformation [in MetaRocq.ErasurePlugin.ETransform]
constructor_isprop_pars_decl [in MetaRocq.Erasure.EGlobalEnv]
construct_cofix_view_sind [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view_rec [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view_ind [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view_rect [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_viewc [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_sind [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_rec [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_ind [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_rect [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_viewc [in MetaRocq.Erasure.EEtaExpanded]
construct_view_sind [in MetaRocq.Erasure.EEtaExpanded]
construct_view_rec [in MetaRocq.Erasure.EEtaExpanded]
construct_view_ind [in MetaRocq.Erasure.EEtaExpanded]
construct_view_rect [in MetaRocq.Erasure.EEtaExpanded]
construct_cofix_view_sind [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_rec [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_ind [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_rect [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_discr [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_sind [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_rec [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_ind [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_rect [in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_sind [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_rec [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_ind [in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_rect [in MetaRocq.PCUIC.Syntax.PCUICViews]
cons_decl [in MetaRocq.PCUIC.PCUICReduction]
context [in MetaRocq.Erasure.EAst]
ContextSet.constraints [in MetaRocq.Common.Universes]
ContextSet.empty [in MetaRocq.Common.Universes]
ContextSet.equal [in MetaRocq.Common.Universes]
ContextSet.Equal [in MetaRocq.Common.Universes]
ContextSet.inter [in MetaRocq.Common.Universes]
ContextSet.inter_spec [in MetaRocq.Common.Universes]
ContextSet.is_empty [in MetaRocq.Common.Universes]
ContextSet.levels [in MetaRocq.Common.Universes]
ContextSet.subset [in MetaRocq.Common.Universes]
ContextSet.Subset [in MetaRocq.Common.Universes]
ContextSet.t [in MetaRocq.Common.Universes]
ContextSet.union [in MetaRocq.Common.Universes]
ContextSet.union_spec [in MetaRocq.Common.Universes]
contextual_closure_sind [in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_rec [in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_ind [in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_rect [in MetaRocq.PCUIC.PCUICReduction]
context_subst_sind [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_rec [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_ind [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_rect [in MetaRocq.PCUIC.PCUICContextSubst]
context_env_clos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_clos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_position [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_hole_choice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_hole_context [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_choice_term [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_choice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_sind [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_rec [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_ind [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_rect [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_size [in MetaRocq.Examples.tauto]
context_to_erased [in MetaRocq.Erasure.Typed.TypeAnnotations]
context_size [in MetaRocq.PCUIC.utils.PCUICSize]
context_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
ConversionError_sind [in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_rec [in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_ind [in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_rect [in MetaRocq.SafeChecker.PCUICErrors]
ConversionResultSummary_sind [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_rec [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_ind [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_rect [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_sind [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_rec [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_ind [in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_rect [in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.All_decls_alpha_pb_sind [in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_rec [in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_ind [in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_rect [in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_ctx_rel [in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_pb_context [in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_pb_decls [in MetaRocq.Common.EnvironmentTyping]
convert [in MetaRocq.SafeChecker.PCUICTypeChecker]
convert_leq [in MetaRocq.Template.Checker]
convSpec [in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_arity_or_not [in MetaRocq.Erasure.Typed.Erasure]
conv_ctx_refl' [in MetaRocq.PCUIC.PCUICCumulativity]
conv_cum [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
conv_pb_relb_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
conv_pb_leqb [in MetaRocq.Common.BasicAst]
conv_pb_sind [in MetaRocq.Common.BasicAst]
conv_pb_rec [in MetaRocq.Common.BasicAst]
conv_pb_ind [in MetaRocq.Common.BasicAst]
conv_pb_rect [in MetaRocq.Common.BasicAst]
conv_ctx_refl' [in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_pb_sind [in MetaRocq.Template.Checker]
conv_pb_rec [in MetaRocq.Template.Checker]
conv_pb_ind [in MetaRocq.Template.Checker]
conv_pb_rect [in MetaRocq.Template.Checker]
conv_decls_prop [in MetaRocq.PCUIC.PCUICCumulProp]
conv_cum_napp [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_pb_relb_gen_proper [in MetaRocq.SafeChecker.PCUICTypeChecker]
cored_sind [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_ind [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored' [in MetaRocq.PCUIC.PCUICSN]
CorrectExtractTransform [in MetaRocq.Erasure.Typed.Transform]
count_ones [in MetaRocq.Erasure.Typed.Optimize]
count_zeros [in MetaRocq.Erasure.Typed.Optimize]
cstr_arity [in MetaRocq.Template.WcbvEval]
cstr_arity [in MetaRocq.Erasure.EAst]
cstr_branch_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
cstr_arity [in MetaRocq.PCUIC.PCUICWcbvEval]
cstr_branch_context [in MetaRocq.Template.Ast]
csubst [in MetaRocq.Erasure.ECSubst]
csubst [in MetaRocq.Template.WcbvEval]
csubst [in MetaRocq.PCUIC.PCUICCSubst]
cs_equal [in MetaRocq.SafeChecker.PCUICSafeChecker]
ctors_info [in MetaRocq.Erasure.Typed.CertifyingEta]
ctxmap [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctx_inst_sub [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_size [in MetaRocq.PCUIC.PCUICTyping]
ctx_inst_size [in MetaRocq.Template.Typing]
cumulAlgo_gen_sind [in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_rec [in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_ind [in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_rect [in MetaRocq.PCUIC.PCUICCumulativity]
cumulP_sind [in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_rec [in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_ind [in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_rect [in MetaRocq.PCUIC.PCUICSubstitution]
cumulSpec [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumulSpec0_ind [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumulSpec0_rec [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_ctx_refl' [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_ctx_refl' [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Construct_univ [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Ind_univ [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_mfixpoint [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_branches [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_branch [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_predicate_dep [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_predicate [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_decl [in MetaRocq.SafeChecker.PCUICSafeChecker]
cumul_gen_sind [in MetaRocq.Template.Typing]
cumul_gen_rec [in MetaRocq.Template.Typing]
cumul_gen_ind [in MetaRocq.Template.Typing]
cumul_gen_rect [in MetaRocq.Template.Typing]
cumul_prop_sind [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_rec [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_ind [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_rect [in MetaRocq.PCUIC.PCUICCumulProp]
cunfold_cofix [in MetaRocq.Template.WcbvEval]
cunfold_fix [in MetaRocq.Template.WcbvEval]
cunfold_cofix [in MetaRocq.Erasure.EGlobalEnv]
cunfold_fix [in MetaRocq.Erasure.EGlobalEnv]
cunfold_cofix [in MetaRocq.PCUIC.PCUICWcbvEval]
cunfold_fix [in MetaRocq.PCUIC.PCUICWcbvEval]
| 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) |