| 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
CannotUnfoldFix [constructor, in MetaRocq.SafeChecker.PCUICErrors]CanonicalTries [library]
canonical_abstract_env_impl [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
canonical_abstract_env_prop [instance, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
canonical_abstract_env_struct [instance, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
can_val_Prop [definition, in MetaRocq.Examples.tauto]
can_val [definition, in MetaRocq.Examples.tauto]
can_have_args [definition, in MetaRocq.Erasure.Typed.ExAst]
cardinality [projection, in MetaRocq.Utils.MRListable]
CaseBranchTypeBeta [section, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseBranchTypeBeta.cf [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseBrsProp [definition, in MetaRocq.PCUIC.Syntax.PCUICInduction]
CaseBrsProp [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
CaseBrsProp_depth [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
CaseDefinitions [section, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.cf [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.ind [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.mib [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.oib [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.pparams [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseDefinitions.puinst [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
CaseOnDifferentInd [constructor, in MetaRocq.SafeChecker.PCUICErrors]
CasePredParamsUnequalLength [constructor, in MetaRocq.SafeChecker.PCUICErrors]
CasePredProp [definition, in MetaRocq.PCUIC.Syntax.PCUICInduction]
CasePredProp [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
CasePredProp_depth [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
CasePredUnequalUniverseInstances [constructor, in MetaRocq.SafeChecker.PCUICErrors]
Case_branch [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Case_discr [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Case_pred [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
case_brsbody [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
case_c [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
case_preturn [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
case_par [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Case_Construct_ind_eq [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
case_branch_info [constructor, in MetaRocq.PCUIC.PCUICTyping]
case_branch_typing [inductive, in MetaRocq.PCUIC.PCUICTyping]
case_side_info [constructor, in MetaRocq.PCUIC.PCUICTyping]
case_side_conditions [inductive, in MetaRocq.PCUIC.PCUICTyping]
case_predicate_context_alpha [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
case_branch_context_nopars [definition, in MetaRocq.PCUIC.PCUICInductiveInversion]
case_branch_type_eq_context_gen_2 [lemma, in MetaRocq.PCUIC.PCUICAlpha]
case_branch_type_eq_context_gen_1 [lemma, in MetaRocq.PCUIC.PCUICAlpha]
case_branch_type_equiv [lemma, in MetaRocq.PCUIC.PCUICAlpha]
case_branch_context_equiv [lemma, in MetaRocq.PCUIC.PCUICAlpha]
case_predicate_context_equiv [lemma, in MetaRocq.PCUIC.PCUICAlpha]
case_info [record, in MetaRocq.Common.BasicAst]
case_predicate_context' [definition, in MetaRocq.PCUIC.PCUICCasesContexts]
case_brs_forallb_map_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
case_brs_map_k_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
case_brs_map_spec_cond [lemma, in MetaRocq.PCUIC.PCUICAst]
case_brs_map_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
case_red_brs [constructor, in MetaRocq.Template.Typing]
case_red_discr [constructor, in MetaRocq.Template.Typing]
case_red_pred_return [constructor, in MetaRocq.Template.Typing]
case_red_pred_param [constructor, in MetaRocq.Template.Typing]
case_inv [constructor, in MetaRocq.PCUIC.PCUICInversion]
case_inversion_data [inductive, in MetaRocq.PCUIC.PCUICInversion]
case_red_brs [constructor, in MetaRocq.PCUIC.PCUICReduction]
case_red_discr [constructor, in MetaRocq.PCUIC.PCUICReduction]
case_red_return [constructor, in MetaRocq.PCUIC.PCUICReduction]
case_red_param [constructor, in MetaRocq.PCUIC.PCUICReduction]
case_branch_type_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branches_contexts_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_assumptions [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_length_args [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context_length_indices [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_type_fst [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_type [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_type_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branches_contexts [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branches_contexts_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
case_conv_preds_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
case_conv_brs_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
case_branch_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
case_branch_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
case_branch_type [definition, in MetaRocq.Template.Ast]
case_branch_type_gen [definition, in MetaRocq.Template.Ast]
case_branches_contexts [definition, in MetaRocq.Template.Ast]
case_branches_contexts_gen [definition, in MetaRocq.Template.Ast]
case_branch_context [definition, in MetaRocq.Template.Ast]
case_branch_context_gen [definition, in MetaRocq.Template.Ast]
case_predicate_context [definition, in MetaRocq.Template.Ast]
case_predicate_context_gen [definition, in MetaRocq.Template.Ast]
case_brs_forallb_map_spec [lemma, in MetaRocq.Template.Ast]
case_brs_map_k_spec [lemma, in MetaRocq.Template.Ast]
case_brs_map_spec [lemma, in MetaRocq.Template.Ast]
case_branch_type_beta_typed [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_conv_beta [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_beta [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_context_unfold [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_subst [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_subst_gen [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_split [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_gen_split [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_only [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_only_gen [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_context [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
Cast [constructor, in MetaRocq.Common.BasicAst]
cast_kind_sind [definition, in MetaRocq.Common.BasicAst]
cast_kind_rec [definition, in MetaRocq.Common.BasicAst]
cast_kind_ind [definition, in MetaRocq.Common.BasicAst]
cast_kind_rect [definition, in MetaRocq.Common.BasicAst]
cast_kind [inductive, in MetaRocq.Common.BasicAst]
cast_red [constructor, in MetaRocq.Template.Typing]
cast_red_r [constructor, in MetaRocq.Template.Typing]
cast_red_l [constructor, in MetaRocq.Template.Typing]
catch [projection, in MetaRocq.Utils.monad_utils]
cbn [constructor, in MetaRocq.Template.TemplateMonad.Common]
cbv [constructor, in MetaRocq.Template.TemplateMonad.Common]
ccview_other [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
ccview_cofix [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
ccview_construct [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
cc_viewc [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
cc0view_other [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
cc0view_cofix [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
cc0view_construct [constructor, in MetaRocq.SafeChecker.PCUICSafeReduce]
cc0_viewc [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
cdecl_Type [definition, in MetaRocq.Examples.tauto]
Certifying [library]
CertifyingBeta [library]
CertifyingEta [library]
CertifyingInlining [library]
cf [section, in MetaRocq.PCUIC.PCUICFirstorder]
cf' [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cf.cf [variable, in MetaRocq.PCUIC.PCUICFirstorder]
change_modpath [definition, in MetaRocq.Erasure.Typed.Certifying]
char63_to_string [definition, in MetaRocq.Utils.Show]
check [definition, in MetaRocq.Template.Checker]
check [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
checkb_constructors_smaller [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
Checked [constructor, in MetaRocq.SafeChecker.PCUICErrors]
Checked [constructor, in MetaRocq.Template.Checker]
Checked_comp [constructor, in MetaRocq.SafeChecker.PCUICErrors]
CheckEnv [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.cf [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.A [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.AA [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.BB [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.f [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.M [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.P [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.Q [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadAllAll.T [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.ext [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.M [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.P [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.T [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.X [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.XX_ext' [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.XX_ext [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadLiftExt.X_ext [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.A [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.B [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.f [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.M [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.MonadMapi.T [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.P [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.A [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.M [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.T [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.BB [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall.AA [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.monad_Alli_nth_forall [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.nor [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.PositivityCheck [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.PositivityCheck.normalization_in [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.PositivityCheck.X_ext [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.UniverseChecks [section, in MetaRocq.SafeChecker.PCUICSafeChecker]
CheckEnv.X_impl [variable, in MetaRocq.SafeChecker.PCUICSafeChecker]
if _ then _ else _ [notation, in MetaRocq.SafeChecker.PCUICSafeChecker]
Checker [section, in MetaRocq.Template.Checker]
Checker [library]
CheckerFlags [section, in MetaRocq.PCUIC.PCUICWfUniverses]
CheckerFlags.cf [variable, in MetaRocq.PCUIC.PCUICWfUniverses]
CheckerFlags.WfUniverses [section, in MetaRocq.PCUIC.PCUICWfUniverses]
CheckerFlags.WfUniverses.Σ [variable, in MetaRocq.PCUIC.PCUICWfUniverses]
checker_flags [record, in MetaRocq.Common.config]
Checker.cf [variable, in MetaRocq.Template.Checker]
Checker.F [variable, in MetaRocq.Template.Checker]
checking [inductive, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_size_pos [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_size [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_sind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_rec [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_ind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_rect [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
checking_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
CheckLeq [section, in MetaRocq.Common.uGraph]
CheckLeqProcedure [section, in MetaRocq.Common.uGraph]
CheckLeqProcedure.cf [variable, in MetaRocq.Common.uGraph]
CheckLeqProcedure.leqb_level_n [variable, in MetaRocq.Common.uGraph]
CheckLeq.cf [variable, in MetaRocq.Common.uGraph]
CheckLeq.G [variable, in MetaRocq.Common.uGraph]
CheckLeq.HC [variable, in MetaRocq.Common.uGraph]
CheckLeq.HG [variable, in MetaRocq.Common.uGraph]
CheckLeq.Huctx [variable, in MetaRocq.Common.uGraph]
CheckLeq.levels_declared_sort [variable, in MetaRocq.Common.uGraph]
CheckLeq.uctx [variable, in MetaRocq.Common.uGraph]
CheckLeq2 [section, in MetaRocq.Common.uGraph]
CheckLeq2.cf [variable, in MetaRocq.Common.uGraph]
CheckLeq2.expr_declared [variable, in MetaRocq.Common.uGraph]
CheckLeq2.G [variable, in MetaRocq.Common.uGraph]
CheckLeq2.HC [variable, in MetaRocq.Common.uGraph]
CheckLeq2.HC' [variable, in MetaRocq.Common.uGraph]
CheckLeq2.HG [variable, in MetaRocq.Common.uGraph]
CheckLeq2.HG' [variable, in MetaRocq.Common.uGraph]
CheckLeq2.Huctx [variable, in MetaRocq.Common.uGraph]
CheckLeq2.Huctx' [variable, in MetaRocq.Common.uGraph]
CheckLeq2.levels_declared_sort [variable, in MetaRocq.Common.uGraph]
CheckLeq2.levels_declared [variable, in MetaRocq.Common.uGraph]
CheckLeq2.level_declared [variable, in MetaRocq.Common.uGraph]
CheckLeq2.uctx [variable, in MetaRocq.Common.uGraph]
check_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
check_Cumul [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
check_univs [projection, in MetaRocq.Common.config]
check_ind_sorts_is_propositional [lemma, in MetaRocq.PCUIC.PCUICElimination]
check_wf_and_extract [definition, in MetaRocq.Erasure.Typed.Extraction]
check_wf_env_func [projection, in MetaRocq.Erasure.Typed.Extraction]
check_inh [definition, in MetaRocq.Examples.typing_correctness]
check_one_cofix [definition, in MetaRocq.PCUIC.PCUICTyping]
check_one_fix [definition, in MetaRocq.PCUIC.PCUICTyping]
check_recursivity_kind [definition, in MetaRocq.PCUIC.PCUICTyping]
check_cmpb_sort_gen [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
check_cmpb_universe_gen [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
check_oib_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
check_eq_nat [definition, in MetaRocq.Utils.monad_utils]
check_eq_true [definition, in MetaRocq.Utils.monad_utils]
check_dec [definition, in MetaRocq.Utils.monad_utils]
check_type_wf_env_fast [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env_bool_spec2 [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env_bool_spec [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_type_wf_env_bool [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_ext [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_decls [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_univs [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_decl [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_one_ind_body [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_ind_types [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_indices [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructors_smallerP [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projections [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projections_cs [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projection [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_projections_type [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructors [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_cstr_variance [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_variance [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_local [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_positive_cstr [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_positive_cstr_arg [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructors_univs [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructor [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_constructor_spec [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_conv_args [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_leq_terms [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_compare_context [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_eq_decl [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_eq_term [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_type_local_ctx [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_context_wf_env [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_type_wf_env [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_env_ext_prop [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_udecl [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_fresh [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_judgement [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_type [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_eq_true_lazy [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
check_wf_eta [definition, in MetaRocq.Template.TemplateCheckWf]
check_wf [definition, in MetaRocq.Template.TemplateCheckWf]
check_def [definition, in MetaRocq.Template.TemplateCheckWf]
check_one_cofix [definition, in MetaRocq.Template.Typing]
check_one_fix [definition, in MetaRocq.Template.Typing]
check_recursivity_kind [definition, in MetaRocq.Template.Typing]
check_dearging_trans [definition, in MetaRocq.ErasurePlugin.ETransform]
check_dearging_precond_spec [lemma, in MetaRocq.ErasurePlugin.ETransform]
check_dearging_precond [definition, in MetaRocq.ErasurePlugin.ETransform]
check_wf_declarations [definition, in MetaRocq.Template.Checker]
check_fresh [definition, in MetaRocq.Template.Checker]
check_wf_decl [definition, in MetaRocq.Template.Checker]
check_wf_judgement [definition, in MetaRocq.Template.Checker]
check_wf_type [definition, in MetaRocq.Template.Checker]
check_consistent_constraints [definition, in MetaRocq.Template.Checker]
check_conv [definition, in MetaRocq.Template.Checker]
check_conv_leq [definition, in MetaRocq.Template.Checker]
check_conv_gen [definition, in MetaRocq.Template.Checker]
check_inh [definition, in MetaRocq.Examples.metarocq_tour_prelude]
check_constraints_complete [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
check_constraints_spec [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
check_recursivity_kind_inj [lemma, in MetaRocq.PCUIC.PCUICClassification]
check_oib_masks_trans [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
check_eqb_sort_complete [definition, in MetaRocq.Common.uGraph]
check_eqb_sort_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_eqb_sort_spec' [definition, in MetaRocq.Common.uGraph]
check_eqb_sort_spec_gen' [lemma, in MetaRocq.Common.uGraph]
check_leqb_sort_complete [definition, in MetaRocq.Common.uGraph]
check_leqb_sort_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_leqb_sort_spec' [definition, in MetaRocq.Common.uGraph]
check_leqb_sort_spec_gen' [lemma, in MetaRocq.Common.uGraph]
check_constraints_complete [definition, in MetaRocq.Common.uGraph]
check_constraints_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_constraints_spec [definition, in MetaRocq.Common.uGraph]
check_constraints_spec_gen [lemma, in MetaRocq.Common.uGraph]
check_gc_constraints_complete [definition, in MetaRocq.Common.uGraph]
check_gc_constraints_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_gc_constraint_complete [definition, in MetaRocq.Common.uGraph]
check_gc_constraint_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_eqb_universe_complete [definition, in MetaRocq.Common.uGraph]
check_eqb_universe_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_eqb_universe_spec' [definition, in MetaRocq.Common.uGraph]
check_eqb_universe_spec_gen' [lemma, in MetaRocq.Common.uGraph]
check_leqb_universe_complete [definition, in MetaRocq.Common.uGraph]
check_leqb_universe_complete_gen [lemma, in MetaRocq.Common.uGraph]
check_leqb_universe_spec' [definition, in MetaRocq.Common.uGraph]
check_leqb_universe_spec_gen' [lemma, in MetaRocq.Common.uGraph]
check_eqb_sort_spec [definition, in MetaRocq.Common.uGraph]
check_eqb_sort_spec_gen [lemma, in MetaRocq.Common.uGraph]
check_eqb_sort_refl [definition, in MetaRocq.Common.uGraph]
check_eqb_sort_refl_gen [lemma, in MetaRocq.Common.uGraph]
check_eqb_sort [definition, in MetaRocq.Common.uGraph]
check_leqb_sort [definition, in MetaRocq.Common.uGraph]
check_gc_constraints_spec [definition, in MetaRocq.Common.uGraph]
check_gc_constraints_spec_gen [lemma, in MetaRocq.Common.uGraph]
check_gc_constraint_spec [definition, in MetaRocq.Common.uGraph]
check_gc_constraint_spec_gen [lemma, in MetaRocq.Common.uGraph]
check_constraints [definition, in MetaRocq.Common.uGraph]
check_gc_constraints [definition, in MetaRocq.Common.uGraph]
check_gc_constraint [definition, in MetaRocq.Common.uGraph]
check_eqb_universe_spec [definition, in MetaRocq.Common.uGraph]
check_eqb_universe_spec_gen [lemma, in MetaRocq.Common.uGraph]
check_eqb_universe [definition, in MetaRocq.Common.uGraph]
check_leqb_universe_spec [definition, in MetaRocq.Common.uGraph]
check_leqb_universe_spec_gen [lemma, in MetaRocq.Common.uGraph]
check_leqb_universe [definition, in MetaRocq.Common.uGraph]
check_eqb_sort_gen [definition, in MetaRocq.Common.uGraph]
check_leqb_sort_gen [definition, in MetaRocq.Common.uGraph]
check_constraints_gen [definition, in MetaRocq.Common.uGraph]
check_gc_constraints_gen [definition, in MetaRocq.Common.uGraph]
check_gc_constraint_gen [definition, in MetaRocq.Common.uGraph]
check_eqb_universe_gen [definition, in MetaRocq.Common.uGraph]
check_leqb_universe_gen [definition, in MetaRocq.Common.uGraph]
check_isType [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_primitive_typing [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_primitive_invariants [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_eq_true [abbreviation, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_mfix_bodies [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_mfix_types [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_branches [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_is_allowed_elimination [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_consistent_instance [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_pb_terms [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_inst [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_alpha_ws_cumul_ctx [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_ctx [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_ws_cumul_pb_decl [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_context_rel [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
check_context [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
choice [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
choice_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
choose_decl_type [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
choose_decl_body [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
chop [definition, in MetaRocq.Utils.MRList]
chop_all [lemma, in MetaRocq.Erasure.EImplementBox]
chop_eq [lemma, in MetaRocq.Erasure.EImplementBox]
chop_firstn_skipn [lemma, in MetaRocq.Erasure.EImplementBox]
chop_n_app [lemma, in MetaRocq.Utils.MRList]
chop_map [lemma, in MetaRocq.Utils.MRList]
chop_all [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
chop_eq [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
chop_firstn_skipn [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
chop_firstn_skipn [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
ci_relevance [projection, in MetaRocq.Common.BasicAst]
ci_npar [projection, in MetaRocq.Common.BasicAst]
ci_ind [projection, in MetaRocq.Common.BasicAst]
classification [lemma, in MetaRocq.PCUIC.PCUICProgress]
classification [section, in MetaRocq.PCUIC.PCUICClassification]
classification.cf [variable, in MetaRocq.PCUIC.PCUICClassification]
classification.wfΣ [variable, in MetaRocq.PCUIC.PCUICClassification]
classification.Σ [variable, in MetaRocq.PCUIC.PCUICClassification]
clear_bit [definition, in MetaRocq.Erasure.Typed.Optimize]
closed [abbreviation, in MetaRocq.PCUIC.PCUICAst]
closed [abbreviation, in MetaRocq.Template.Ast]
closed [abbreviation, in MetaRocq.Erasure.ELiftSubst]
ClosedAux [library]
closedn [definition, in MetaRocq.PCUIC.PCUICAst]
closedn [definition, in MetaRocq.Template.Ast]
closedn [definition, in MetaRocq.Erasure.ELiftSubst]
closedn_ctx_subst_forall [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
closedn_ctx_lift_inv [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
closedn_All_local_closed [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closedn_All_local_env [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closedn_ctx_alpha [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closedn_zip [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_fill_hole [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_stack [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_stack_entry [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_branches_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_predicate_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_context_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_mfix_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_expand_lets [lemma, in MetaRocq.PCUIC.PCUICSR]
closedn_subst0 [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closedn_subst [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closedn_lift [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closedn_mkApps [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closedn_to_extended_list [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_to_extended_list_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_to_extended_list_k_up [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_upwards [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_expand_lets [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_extended_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_extended_subst_gen [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_decl [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mapi_rec_ext [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_smash_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_spec [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_instance_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_tip [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_eq' [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_lift_inv [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_cons [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closedn_ctx_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closedn_expand'' [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedn_expand' [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedn_expand [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedn_mkApps [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
closedn_ctx_snoc [lemma, in MetaRocq.PCUIC.PCUICContexts]
closedn_ctx [abbreviation, in MetaRocq.PCUIC.PCUICAst]
closedn_mkApps [lemma, in MetaRocq.Erasure.EWcbvEval]
closedn_mkApps [lemma, in MetaRocq.PCUIC.PCUICClassification]
closedn_dearg_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_dearg_case_branch_body_rec [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_dearg_single [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_ctx_cstr_branch_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closedn_ctx_expand_lets [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closedn_mkApps [lemma, in MetaRocq.Erasure.ERemoveParams]
closedn_ctx_on_free_vars_shift [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_ctx_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_subst [lemma, in MetaRocq.Erasure.ELiftSubst]
closedn_subst_eq [lemma, in MetaRocq.Erasure.ELiftSubst]
closedn_lift [lemma, in MetaRocq.Erasure.ELiftSubst]
closedP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP_eq [lemma, in MetaRocq.PCUIC.PCUICSR]
closedP_mon [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closedP_xpredT [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
ClosedSpineSubst [section, in MetaRocq.PCUIC.PCUICSpine]
ClosedSpineSubst.cf [variable, in MetaRocq.PCUIC.PCUICSpine]
Closedu [section, in MetaRocq.Common.Universes]
closedu [definition, in MetaRocq.PCUIC.PCUICAst]
closedu [definition, in MetaRocq.Template.Ast]
closedu_subst_instance [lemma, in MetaRocq.Common.Universes]
closedu_subst_instance_univ [lemma, in MetaRocq.Common.Universes]
closedu_subst_instance_level_expr [lemma, in MetaRocq.Common.Universes]
closedu_subst_instance_level [lemma, in MetaRocq.Common.Universes]
closedu_instance [definition, in MetaRocq.Common.Universes]
closedu_sort [definition, in MetaRocq.Common.Universes]
closedu_universe [definition, in MetaRocq.Common.Universes]
closedu_level_expr [definition, in MetaRocq.Common.Universes]
closedu_level [definition, in MetaRocq.Common.Universes]
closedu_subst_instance_cstrs_lift [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_cstrs_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_cstrs [definition, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_cstr [definition, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_lift [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_expr_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_lift [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
closedu_subst_instance [lemma, in MetaRocq.Template.UnivSubst]
closedu_inds [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_reln [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_smash_context [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_smash_context_gen [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_extended_subst [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_lift_context [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_subst_context [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_subst [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_lift [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_ctx [abbreviation, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_abstract_instance [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_mkApps [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_compare_decls [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
Closedu.k [variable, in MetaRocq.Common.Universes]
closed_fake_params [lemma, in MetaRocq.PCUIC.PCUICNormal]
closed_cstr_branch_context_gen [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closed_red1_ctx [definition, in MetaRocq.PCUIC.PCUICSR]
closed_red1_case_branch_type [lemma, in MetaRocq.PCUIC.PCUICSR]
closed_red1_mkApps_left [lemma, in MetaRocq.PCUIC.PCUICSR]
closed_red1_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSR]
closed_red1_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICSR]
closed_red1_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICSR]
closed_red1_ind' [definition, in MetaRocq.PCUIC.PCUICSR]
closed_red1_ind [lemma, in MetaRocq.PCUIC.PCUICSR]
closed_nlctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
closed_nl [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
closed_ctx_IH [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
closed_upwards [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
closed_implement_box [lemma, in MetaRocq.Erasure.EImplementBox]
closed_csubst [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps_args [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps_head [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps_inv [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps [lemma, in MetaRocq.Erasure.Typed.ClosedAux]
closed_tele_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
closed_ctx_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
closed_ctx_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ind_closed_cstrs [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_inds [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ind_predicate_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ctx_decl [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ctx_expand_lets [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_declared_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_inductive_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_inductive_body [definition, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_constructor_body [definition, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_smash_context_unfold [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_smash_context_gen [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_subst_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_map_subst_instance [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ctx_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_decl_upwards [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_spine_subst_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
closed_spine_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
closed_subslet [lemma, in MetaRocq.PCUIC.PCUICSpine]
closed_subst_map_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
closed_ctx_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
closed_k_ctx_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
closed_red1_red [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red_open_right [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red_red [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red1_open_right [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red1_red1 [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red1 [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_relation [record, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_substl [lemma, in MetaRocq.Erasure.ECSubst]
closed_csubst [lemma, in MetaRocq.Erasure.ECSubst]
closed_subst [lemma, in MetaRocq.Erasure.ECSubst]
closed_context_conversion [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_cumulativity [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_conv_conv [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_cumul_cumul [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_red_ctx_refl [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_refl [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_eq_context_upto_r [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_eq_context_upto_l [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_confluence [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_compare_term_r [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_compare_term_l [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_trans [instance, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_ctx_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_ctx [definition, in MetaRocq.PCUIC.PCUICContextConversion]
closed_context [abbreviation, in MetaRocq.PCUIC.PCUICConfluence]
closed_term [abbreviation, in MetaRocq.PCUIC.PCUICConfluence]
closed_cunfold_cofix [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_cunfold_fix [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_iota_red [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_unfold_cofix [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_unfold_fix [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_constant [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closed_ctx_is_closed_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closed_csubst [lemma, in MetaRocq.PCUIC.PCUICCSubst]
closed_subst [lemma, in MetaRocq.PCUIC.PCUICCSubst]
closed_subst [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
closed_upwards [lemma, in MetaRocq.Template.LiftSubst]
closed_red_mkApps [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
closed_red_rel_all [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red1_mkApps_left [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_terms_open_right [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_terms_open_left [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_prod_codom [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_letin_body [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_letin [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_untyped_substitution0 [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_untyped_substitution [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_red_subst0 [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_red_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_red_clos [lemma, in MetaRocq.PCUIC.PCUICConversion]
closed_prod_type [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
closed_eprogram_env [definition, in MetaRocq.Erasure.EProgram]
closed_eprogram [definition, in MetaRocq.Erasure.EProgram]
closed_ctx [abbreviation, in MetaRocq.PCUIC.PCUICAst]
closed_decl [abbreviation, in MetaRocq.PCUIC.PCUICAst]
closed_iota_red [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
closed_remove_match_on_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
closed_iota_red [lemma, in MetaRocq.Erasure.EReorderCstrs]
closed_transform_blocks [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
closed_cunfold_cofix [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_cunfold_fix [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_cofix_subst [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_fix_subst [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_unfold_cofix_cunfold_eq [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_cofix_substl_subst_eq [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_unfold_fix_cunfold_eq [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_fix_substl_subst_eq [lemma, in MetaRocq.Erasure.EWcbvEval]
closed_ctx_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
closed_red_upto_conv_ctx_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
closed_red1_upto_conv_ctx_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
closed_iota_red [lemma, in MetaRocq.Erasure.EInlineProjections]
closed_red_red [definition, in MetaRocq.PCUIC.PCUICConvCumInversion]
closed_ind_predicate_context [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
closed_red_zipp [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
closed_red_mkApps_tConst_axiom [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
closed_env [definition, in MetaRocq.Erasure.EGlobalEnv]
closed_decl [definition, in MetaRocq.Erasure.EGlobalEnv]
closed_unfold_cofix [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_unfold_cofix_cunfold_eq [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_unfold_fix_cunfold_eq [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_cofix_substl_subst_eq [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_fix_substl_subst_eq [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_unfold_fix [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_arg [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_iota [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_def [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_beta [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
closed_subst_up_vdef [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_up_vass [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_app_up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_Up' [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_Up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_ctx_args [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_tele_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_strip [lemma, in MetaRocq.Erasure.ERemoveParams]
closed_ctx_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_decl_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_on_free_vars_none [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_arities_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
closed_ind_predicate_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
closed_cstr_branch_context_npars [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_cstr_branch_context [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_ctx_on_ctx_free_vars [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_wf_local [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_upwards [lemma, in MetaRocq.Erasure.ELiftSubst]
closed_iota_red [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
closed_trans [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
clos_rt_red1_red1_rel_alpha [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_to_1n [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_sind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_rec [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_ind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n_rect [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_1n [inductive, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_alpha_out' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_alpha_out [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_red1 [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_ws_red1 [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_red_rel_out_inv [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_red_rel_out [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_out [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_red1_ctx_eq_length [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_prod_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_prod_l_sigma [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_rt_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_ctx_rt_ctx_red1_rel [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_length [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_prod_r [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_prod_l [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_disjunction_right [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_disjunction_left [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_monotone [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_trans [instance, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_sind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_rec [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_ind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_rect [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t [inductive, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_OnOne2_local_env_ctx_incl [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_trans [instance, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_sind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_rec [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_ind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_rect [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx [inductive, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_sind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_rec [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_ind [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl_rect [definition, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_decl [inductive, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_proper [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_OnOne2_local_env_incl [lemma, in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_sym_trans_Transitive [instance, in MetaRocq.Utils.MRRelations]
clos_refl_sym_trans_Reflexive [instance, in MetaRocq.Utils.MRRelations]
clos_refl_sym_trans_Symmetric [instance, in MetaRocq.Utils.MRRelations]
clos_sym_Symmetric [instance, in MetaRocq.Utils.MRRelations]
clos_sym [definition, in MetaRocq.Utils.MRRelations]
clos_rt_trans_Symmetric [instance, in MetaRocq.Utils.MRRelations]
clos_t_rt_equiv [lemma, in MetaRocq.Utils.MRRelations]
clos_t_rt_incl [lemma, in MetaRocq.Utils.MRRelations]
clos_rt_t_incl [lemma, in MetaRocq.Utils.MRRelations]
clos_refl_trans_prod_r [lemma, in MetaRocq.Utils.MRRelations]
clos_refl_trans_prod_l [lemma, in MetaRocq.Utils.MRRelations]
clos_rt_refl [instance, in MetaRocq.Utils.MRRelations]
clos_rt_trans [instance, in MetaRocq.Utils.MRRelations]
clos_rt_disjunction_right [lemma, in MetaRocq.Utils.MRRelations]
clos_rt_disjunction_left [lemma, in MetaRocq.Utils.MRRelations]
clos_rt_monotone [definition, in MetaRocq.Utils.MRRelations]
clos_t_rt [lemma, in MetaRocq.Utils.MRRelations]
clrel_rel [projection, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
clrel_src [projection, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
clrel_ctx [projection, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
cls_is_true [record, in MetaRocq.Quotation.CommonUtils]
cls_is_true [inductive, in MetaRocq.Quotation.CommonUtils]
cmpb_term_correct [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
cmpb_term [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
cmpb_term_napp [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
cmp_global_instance_cstr_irrelevant [lemma, in MetaRocq.PCUIC.PCUICSR]
cmp_global_instance_nl [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
cmp_global_instance_flip [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_flip [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_flip [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_flip [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_eq [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_empty_impl [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_impl [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_impl_same_napp [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_antisym [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_antisym [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_antisym [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_equiv [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_antisym [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_equiv [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_impl' [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_ind_universes [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
cmp_global_instance_gen [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance_or_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance_length [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance_var_dec [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_instance_opt_variance [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_instance_variance [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_universe_variance [lemma, in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_dep [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance [definition, in MetaRocq.PCUIC.PCUICEquality]
cmp_sort_config_impl [lemma, in MetaRocq.Common.Universes]
cmp_universe_config_impl [lemma, in MetaRocq.Common.Universes]
cmp_sort_subset [lemma, in MetaRocq.Common.Universes]
cmp_universe_subset [lemma, in MetaRocq.Common.Universes]
cmp_global_instance_weaken_env [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cmp_global_instance_impl [instance, in MetaRocq.Template.TermEquality]
cmp_global_instance_impl_same_napp [instance, in MetaRocq.Template.TermEquality]
cmp_global_instance_refl [lemma, in MetaRocq.Template.TermEquality]
cmp_universe_instance_refl [lemma, in MetaRocq.Template.TermEquality]
cmp_universe_instance_variance_impl [lemma, in MetaRocq.Template.TermEquality]
cmp_universe_instance_impl' [lemma, in MetaRocq.Template.TermEquality]
cmp_universe_instance_impl [lemma, in MetaRocq.Template.TermEquality]
cmp_global_instance [abbreviation, in MetaRocq.Template.TermEquality]
cmp_global_instance_gen [definition, in MetaRocq.Template.TermEquality]
cmp_opt_variance_var_dec [lemma, in MetaRocq.Template.TermEquality]
cmp_instance_variance [lemma, in MetaRocq.Template.TermEquality]
cmp_universe_universe_variance [lemma, in MetaRocq.Template.TermEquality]
cmp_instance_opt_variance [lemma, in MetaRocq.Template.TermEquality]
cmp_opt_variance [definition, in MetaRocq.Template.TermEquality]
cmp_universe_instance_variance [definition, in MetaRocq.Template.TermEquality]
cmp_universe_variance [definition, in MetaRocq.Template.TermEquality]
cmp_universe_instance [definition, in MetaRocq.Template.TermEquality]
cmp_global_instance_refl_wf [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
cmp_universe_instance_refl_wf [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
cmp_global_instance_ind_inv [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
cmp_universe_instance_variance_irrelevant [lemma, in MetaRocq.PCUIC.PCUICConversion]
cmp_global_instance_length [lemma, in MetaRocq.PCUIC.PCUICConversion]
cmp_True_instance [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cmp_True_subst_instance [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cnat [inductive, in MetaRocq.Examples.demo]
cod [definition, in MetaRocq.Erasure.ErasureFunction]
CoFinite [constructor, in MetaRocq.Common.BasicAst]
CoFix [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
CoFix [constructor, in MetaRocq.PCUIC.PCUICTyping]
CoFixMfixMismatch [constructor, in MetaRocq.SafeChecker.PCUICErrors]
CoFixRargMismatch [constructor, in MetaRocq.SafeChecker.PCUICErrors]
CoFix_app [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
cofix_mfix_bd [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
cofix_mfix_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
cofix_subst_nth [lemma, in MetaRocq.Erasure.Prelim]
cofix_guard_rename [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_inst [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_context_cumulativity [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_extends [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_subst_instance [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_eq_term [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard_red1 [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
cofix_guard [definition, in MetaRocq.PCUIC.PCUICTyping]
cofix_guard_trans [axiom, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cofix_guard_extends [projection, in MetaRocq.Template.Typing]
cofix_guard_subst_instance [projection, in MetaRocq.Template.Typing]
cofix_guard_subst [projection, in MetaRocq.Template.Typing]
cofix_guard_lift [projection, in MetaRocq.Template.Typing]
cofix_guard_red1 [projection, in MetaRocq.Template.Typing]
cofix_guard [projection, in MetaRocq.Template.Typing]
cofix_red_body [constructor, in MetaRocq.Template.Typing]
cofix_red_ty [constructor, in MetaRocq.Template.Typing]
cofix_subst_length [lemma, in MetaRocq.Template.Typing]
cofix_subst [definition, in MetaRocq.Template.Typing]
cofix_to_lazy [projection, in MetaRocq.ErasurePlugin.Erasure]
cofix_red_body [constructor, in MetaRocq.PCUIC.PCUICReduction]
cofix_red_ty [constructor, in MetaRocq.PCUIC.PCUICReduction]
cofix_subst_instance_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cofix_subst_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
cofix_subst_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
cofix_subst [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
cofix_guard_trans [axiom, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
cofix_subst_length [lemma, in MetaRocq.Erasure.EGlobalEnv]
cofix_subst [definition, in MetaRocq.Erasure.EGlobalEnv]
cofix_guard_trans [axiom, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
CoIndFix [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
coinductive_to_inductive_transformation_ext' [instance, in MetaRocq.ErasurePlugin.ETransform]
coinductive_to_inductive_transformation_ext [instance, in MetaRocq.ErasurePlugin.ETransform]
coinductive_to_inductive_transformation [definition, in MetaRocq.ErasurePlugin.ETransform]
combine_map_id [lemma, in MetaRocq.Utils.MRList]
combine_valuations [definition, in MetaRocq.Common.UniversesDec]
Common [library]
CommonUtils [library]
Common_kn [definition, in MetaRocq.Template.TemplateMonad.Core]
common_prefix [definition, in MetaRocq.Quotation.CommonUtils]
common_prefix_ls [definition, in MetaRocq.Quotation.CommonUtils]
common_typing [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
commutes [definition, in MetaRocq.Utils.MRRelations]
commutes_disj_joinable [lemma, in MetaRocq.PCUIC.PCUICConfluence]
commutes_diamonds_diamond [lemma, in MetaRocq.PCUIC.PCUICConfluence]
commut_lift_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
commut_lift_subst_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
commut_lift_subst [lemma, in MetaRocq.Template.LiftSubst]
commut_lift_subst_rec [lemma, in MetaRocq.Template.LiftSubst]
commut_lift_subst [lemma, in MetaRocq.Erasure.ELiftSubst]
commut_lift_subst_rec [lemma, in MetaRocq.Erasure.ELiftSubst]
compare [definition, in MetaRocq.Utils.ByteCompare]
CompareSpec_Proper [lemma, in MetaRocq.Utils.MRCompare]
CompareSpec_string [abbreviation, in MetaRocq.Utils.bytestring]
compare_eq_refl [lemma, in MetaRocq.Utils.ByteCompareSpec]
compare_spec [lemma, in MetaRocq.Utils.ByteCompareSpec]
compare_eq [lemma, in MetaRocq.Utils.ByteCompareSpec]
compare_opp [lemma, in MetaRocq.Utils.ByteCompareSpec]
compare_equiv [lemma, in MetaRocq.Utils.ByteCompareSpec]
compare_decls_lift_decl [lemma, in MetaRocq.PCUIC.PCUICEquality]
compare_term_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
compare_term_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
compare_term_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
compare_context [definition, in MetaRocq.PCUIC.PCUICEquality]
compare_decl [definition, in MetaRocq.PCUIC.PCUICEquality]
compare_opt_term [definition, in MetaRocq.PCUIC.PCUICEquality]
compare_term [definition, in MetaRocq.PCUIC.PCUICEquality]
compare_term_napp [definition, in MetaRocq.PCUIC.PCUICEquality]
compare_decl_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
compare_decl_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
compare_decl_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
compare_decl_map [lemma, in MetaRocq.PCUIC.PCUICEquality]
compare_decl_impl_ondecl [lemma, in MetaRocq.PCUIC.PCUICEquality]
compare_decls_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
compare_decls [definition, in MetaRocq.PCUIC.PCUICEquality]
compare_vdef [constructor, in MetaRocq.PCUIC.PCUICEquality]
compare_vass [constructor, in MetaRocq.PCUIC.PCUICEquality]
compare_cont_trans [lemma, in MetaRocq.Utils.MRCompare]
compare_cont_CompOpp [lemma, in MetaRocq.Utils.MRCompare]
compare_cont [definition, in MetaRocq.Utils.MRCompare]
compare_sort_preorder [instance, in MetaRocq.Common.Universes]
compare_sort_trans [instance, in MetaRocq.Common.Universes]
compare_sort_refl [instance, in MetaRocq.Common.Universes]
compare_sort_subrel [instance, in MetaRocq.Common.Universes]
compare_sort_type [lemma, in MetaRocq.Common.Universes]
compare_sort [definition, in MetaRocq.Common.Universes]
compare_universe_preorder [instance, in MetaRocq.Common.Universes]
compare_universe_trans [instance, in MetaRocq.Common.Universes]
compare_universe_refl [instance, in MetaRocq.Common.Universes]
compare_universe_subrel [instance, in MetaRocq.Common.Universes]
compare_universe [definition, in MetaRocq.Common.Universes]
compare_context_subset [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_decl_subset [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_term_subset [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_term [definition, in MetaRocq.Template.TermEquality]
compare_vdef [constructor, in MetaRocq.Template.TermEquality]
compare_vass [constructor, in MetaRocq.Template.TermEquality]
compare_sortP_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universeP_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance_refl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance_proper [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance_impl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universe_instance_variance [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universe_instance [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universe_variance [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_context_cumul_pb_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
compare_context [definition, in MetaRocq.PCUIC.PCUICContextConversion]
compare_sort_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
compare_term_mkApps_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
compare_term_mkApps_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
compare_ident [definition, in MetaRocq.Common.Kernames]
compare_context_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_decl_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_decls_subst_preserved [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_term_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_sort_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_universe_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_sort_substu [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_universe_substu [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_context_config_impl [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
compare_decl_config_impl [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
compare_term_config_impl [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
compare_global_instance_correct [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universe_instance_variance_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universe_variance_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universeb_make_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universeb_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_decls_refl [instance, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
comparison_trans [definition, in MetaRocq.Utils.MRCompare]
compile_value_erase_mkApps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
compile_value_erase [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
compile_evalue_strip [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_firstorder [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_erase [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_mkApps [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_strip_mkApps [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_value_box_mkApps [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_strip [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_app [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_value_box [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
complete_ctx_mask_length [lemma, in MetaRocq.Erasure.Typed.Optimize]
complete_ctx_mask [definition, in MetaRocq.Erasure.Typed.Optimize]
compose_transforms_correct [lemma, in MetaRocq.Erasure.Typed.Transform]
compose_transforms [definition, in MetaRocq.Erasure.Typed.Transform]
compose_ren [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
compose_ids_l [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
compose_ids_r [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
compose_map_decl [lemma, in MetaRocq.Common.BasicAst]
compose_map_def [lemma, in MetaRocq.Common.BasicAst]
compose_on_snd [lemma, in MetaRocq.Utils.MRProd]
compose_map_def [lemma, in MetaRocq.Erasure.ELiftSubst]
Computational [definition, in MetaRocq.PCUIC.PCUICElimination]
computational_type [definition, in MetaRocq.Erasure.Extract]
computational_ind [definition, in MetaRocq.Erasure.Extract]
compute_masks [definition, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
compute_masks [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
concat_sing [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
concl [projection, in MetaRocq.Examples.tauto]
concrete_sort [definition, in MetaRocq.Common.Universes]
config [library]
ConfluenceFacts [section, in MetaRocq.PCUIC.PCUICConfluence]
ConfluenceFacts.cf [variable, in MetaRocq.PCUIC.PCUICConfluence]
ConfluenceFacts.wfΣ [variable, in MetaRocq.PCUIC.PCUICConfluence]
ConfluenceFacts.Σ [variable, in MetaRocq.PCUIC.PCUICConfluence]
confluent [definition, in MetaRocq.PCUIC.PCUICConfluence]
confluent_union [lemma, in MetaRocq.PCUIC.PCUICConfluence]
confluent_proper [instance, in MetaRocq.PCUIC.PCUICConfluence]
consistent [definition, in MetaRocq.Common.Universes]
consistent_extension_on_union [lemma, in MetaRocq.Common.Universes]
consistent_extension_on_empty [lemma, in MetaRocq.Common.Universes]
consistent_extension_on [definition, in MetaRocq.Common.Universes]
consistent_instance_wf_sort [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
consistent_extension_on_dec [definition, in MetaRocq.Common.UniversesDec]
consistent_extension_on_iff [lemma, in MetaRocq.Common.UniversesDec]
consistent_extension_on_iff_subgraph_helper [lemma, in MetaRocq.Common.UniversesDec]
consistent_extension_on_iff_declare_and_uniquify_and_combine_levels [lemma, in MetaRocq.Common.UniversesDec]
consistent_dec [definition, in MetaRocq.Common.UniversesDec]
consistent_instance_valid [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
consistent_instance_poly_length [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
consistent_extension_on_global [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
consistent_proper [instance, in MetaRocq.SafeChecker.PCUICWfEnv]
consistent_instance_ext_subst_abs_inds [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs_univ [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs_level [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_abstract_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_valid_constraints [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans_polymorphic_cases [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans_polymorphic_case_aux [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_declared [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_wf [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
consistent_instance_ext_wf [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
consistent_ext_on_full_ext [lemma, in MetaRocq.Common.uGraph]
consistent_ext_on_full_ext0 [lemma, in MetaRocq.Common.uGraph]
consistent_no_loop [instance, in MetaRocq.Common.uGraph]
constansts_info [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
ConstantDecl [constructor, in MetaRocq.Erasure.Typed.ExAst]
ConstantDecl [constructor, in MetaRocq.Erasure.EAst]
Constants [library]
constants_inlining [definition, in MetaRocq.Erasure.EInlining]
constant_body_annots [definition, in MetaRocq.Erasure.Typed.Annotations]
constant_decls_deps [definition, in MetaRocq.Erasure.ErasureFunction]
constant_body [record, in MetaRocq.Erasure.Typed.ExAst]
constant_entry_sind [definition, in MetaRocq.PCUIC.PCUICAst]
constant_entry_rec [definition, in MetaRocq.PCUIC.PCUICAst]
constant_entry_ind [definition, in MetaRocq.PCUIC.PCUICAst]
constant_entry_rect [definition, in MetaRocq.PCUIC.PCUICAst]
constant_entry [inductive, in MetaRocq.PCUIC.PCUICAst]
constant_body [record, in MetaRocq.Erasure.EAst]
constant_entry_sind [definition, in MetaRocq.Erasure.EAst]
constant_entry_rec [definition, in MetaRocq.Erasure.EAst]
constant_entry_ind [definition, in MetaRocq.Erasure.EAst]
constant_entry_rect [definition, in MetaRocq.Erasure.EAst]
constant_entry [inductive, in MetaRocq.Erasure.EAst]
constant_entry_sind [definition, in MetaRocq.Template.Ast]
constant_entry_rec [definition, in MetaRocq.Template.Ast]
constant_entry_ind [definition, in MetaRocq.Template.Ast]
constant_entry_rect [definition, in MetaRocq.Template.Ast]
constant_entry [inductive, in MetaRocq.Template.Ast]
ConstraintSet [module, in MetaRocq.Common.Universes]
ConstraintSetDecide [module, in MetaRocq.Common.Universes]
ConstraintSetExtraDecide [module, in MetaRocq.Common.Universes]
ConstraintSetExtraOrdProp [module, in MetaRocq.Common.Universes]
ConstraintSetFact [module, in MetaRocq.Common.Universes]
ConstraintSetOrdProp [module, in MetaRocq.Common.Universes]
ConstraintSetProp [module, in MetaRocq.Common.Universes]
ConstraintSetsUIP [module, in MetaRocq.Common.Reflect]
ConstraintSetsUIP.cs_tree_reflect [instance, in MetaRocq.Common.Reflect]
ConstraintSetsUIP.cs_tree_rect [definition, in MetaRocq.Common.Reflect]
ConstraintSetsUIP.cs_tree_eqb [definition, in MetaRocq.Common.Reflect]
ConstraintSetsUIP.eqb_ConstraintSet [definition, in MetaRocq.Common.Reflect]
ConstraintSetsUIP.ok_irrel [lemma, in MetaRocq.Common.Reflect]
ConstraintSetsUIP.reflect_ConstraintSet [instance, in MetaRocq.Common.Reflect]
ConstraintSet_In__declare_and_uniquify_levels_2__1 [lemma, in MetaRocq.Common.UniversesDec]
ConstraintSet_In__declare_and_uniquify_and_combine_levels_2__0 [lemma, in MetaRocq.Common.UniversesDec]
ConstraintSet_In__declare_and_uniquify_and_combine_levels_1__1 [lemma, in MetaRocq.Common.UniversesDec]
ConstraintSet_In__declare_and_uniquify_and_combine_levels_1__0 [lemma, in MetaRocq.Common.UniversesDec]
ConstraintSet_In_fold_add [lemma, in MetaRocq.Common.UniversesDec]
constraints_of_udecl [definition, in MetaRocq.Common.Universes]
ConstraintType [module, in MetaRocq.Common.Universes]
ConstraintType.compare [definition, in MetaRocq.Common.Universes]
ConstraintType.compare_spec [lemma, in MetaRocq.Common.Universes]
ConstraintType.eq [definition, in MetaRocq.Common.Universes]
ConstraintType.Eq [constructor, in MetaRocq.Common.Universes]
ConstraintType.eq_dec [lemma, in MetaRocq.Common.Universes]
ConstraintType.eq_equiv [definition, in MetaRocq.Common.Universes]
ConstraintType.Le [constructor, in MetaRocq.Common.Universes]
ConstraintType.LeEq [constructor, in MetaRocq.Common.Universes]
ConstraintType.LeLe [constructor, in MetaRocq.Common.Universes]
ConstraintType.Le0 [definition, in MetaRocq.Common.Universes]
ConstraintType.lt [definition, in MetaRocq.Common.Universes]
ConstraintType.Lt [definition, in MetaRocq.Common.Universes]
ConstraintType.lt_compat [instance, in MetaRocq.Common.Universes]
ConstraintType.lt_strorder [instance, in MetaRocq.Common.Universes]
ConstraintType.lt__sind [definition, in MetaRocq.Common.Universes]
ConstraintType.lt__ind [definition, in MetaRocq.Common.Universes]
ConstraintType.lt_ [inductive, in MetaRocq.Common.Universes]
ConstraintType.t [definition, in MetaRocq.Common.Universes]
ConstraintType.t__sind [definition, in MetaRocq.Common.Universes]
ConstraintType.t__rec [definition, in MetaRocq.Common.Universes]
ConstraintType.t__ind [definition, in MetaRocq.Common.Universes]
ConstraintType.t__rect [definition, in MetaRocq.Common.Universes]
ConstraintType.t_ [inductive, in MetaRocq.Common.Universes]
constraint_lt_irrel [lemma, in MetaRocq.Common.Reflect]
constraint_type_lt_level_irrel [lemma, in MetaRocq.Common.Reflect]
constraint_lt_ind_dep [definition, in MetaRocq.Common.Reflect]
constraint_type_lt_ind_dep [definition, in MetaRocq.Common.Reflect]
ConstRef [constructor, in MetaRocq.Common.Kernames]
constructor [definition, in MetaRocq.Examples.constructor_tac]
constructors_as_blocks_transformation_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
constructors_as_blocks_transformation_pres [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
constructors_as_blocks_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
constructors_as_blocks_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
constructors_as_blocks_transformation [definition, in MetaRocq.ErasurePlugin.ETransform]
constructor_isprop_pars_decl_params [lemma, in MetaRocq.Erasure.EImplementBox]
constructor_declared [lemma, in MetaRocq.Template.EtaExpand]
constructor_isprop_pars_decl_constructor [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
constructor_isprop_pars_decl_inductive [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
constructor_cumulative_indices [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
constructor_isprop_pars_decl_inductive [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
constructor_isprop_pars_decl_constructor [lemma, in MetaRocq.Erasure.EGenericMapEnv]
constructor_isprop_pars_decl_inductive [lemma, in MetaRocq.Erasure.EGenericMapEnv]
constructor_isprop_pars_decl_constructor [lemma, in MetaRocq.Erasure.EReorderCstrs]
constructor_isprop_pars_decl_inductive [lemma, in MetaRocq.Erasure.EReorderCstrs]
constructor_isprop_pars_decl_params [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
constructor_body [record, in MetaRocq.Erasure.EAst]
constructor_isprop_pars_decl_in_env [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
constructor_isprop_pars_decl_constructor [lemma, in MetaRocq.Erasure.EInlineProjections]
constructor_isprop_pars_decl_inductive [lemma, in MetaRocq.Erasure.EInlineProjections]
constructor_isprop_pars_decl_trans_env_debox_types [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
constructor_isprop_pars_decl_trans_env_dearg_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
constructor_isprop_pars_decl [definition, in MetaRocq.Erasure.EGlobalEnv]
constructor_isprop_pars_inductive_pars [lemma, in MetaRocq.Erasure.ERemoveParams]
constructor_isprop_pars_decl_lookup [lemma, in MetaRocq.Erasure.ERemoveParams]
constructor_isprop_pars_decl_constructor [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
constructor_isprop_pars_decl_inductive [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
constructor_tac [library]
ConstructRef [constructor, in MetaRocq.Common.Kernames]
construct_cofix_view_sind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view_rec [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view_ind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view_rect [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_cofix_view [inductive, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_viewc [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_sind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_rec [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_ind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view_rect [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_view [inductive, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct_viewc [definition, in MetaRocq.Erasure.EEtaExpanded]
construct_view_sind [definition, in MetaRocq.Erasure.EEtaExpanded]
construct_view_rec [definition, in MetaRocq.Erasure.EEtaExpanded]
construct_view_ind [definition, in MetaRocq.Erasure.EEtaExpanded]
construct_view_rect [definition, in MetaRocq.Erasure.EEtaExpanded]
construct_view [inductive, in MetaRocq.Erasure.EEtaExpanded]
Construct_Ind_ind_eq' [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
Construct_Ind_ind_eq [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
construct_cofix_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
construct_cofix_discr_match [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_other [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_cofix [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_construct [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_view [inductive, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct_cofix_discr [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_sind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_rec [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_ind [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_rect [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view [inductive, in MetaRocq.SafeChecker.PCUICSafeReduce]
construct0_cofix_view_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_other [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_cofix [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_construct [constructor, in MetaRocq.PCUIC.Syntax.PCUICViews]
construct0_cofix_view [inductive, in MetaRocq.PCUIC.Syntax.PCUICViews]
const_masks [projection, in MetaRocq.Erasure.Typed.Optimize]
cons_prefix [lemma, in MetaRocq.Utils.MRList]
cons_let_def [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
cons_let_ass [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
cons_ass [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
cons_decl [definition, in MetaRocq.PCUIC.PCUICReduction]
context [abbreviation, in MetaRocq.Common.BasicAst]
context [abbreviation, in MetaRocq.Common.BasicAst]
context [definition, in MetaRocq.Erasure.EAst]
context [abbreviation, in MetaRocq.Common.MonadBasicAst]
ContextChangeTypesReduction [section, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
ContextChangeTypesReduction.cf [variable, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
ContextChangeTypesReduction.Σ [variable, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
ContextConversion [section, in MetaRocq.PCUIC.PCUICCumulativity]
ContextConversion [section, in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion [section, in MetaRocq.PCUIC.PCUICCumulativitySpec]
ContextConversion.cf [variable, in MetaRocq.PCUIC.PCUICCumulativity]
ContextConversion.cf [variable, in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion.cf [variable, in MetaRocq.PCUIC.PCUICCumulativitySpec]
ContextConversion.wfΣ [variable, in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion.Σ [variable, in MetaRocq.PCUIC.PCUICCumulativity]
ContextConversion.Σ [variable, in MetaRocq.PCUIC.PCUICContextConversion]
ContextConversion.Σ [variable, in MetaRocq.PCUIC.PCUICCumulativitySpec]
ContextMap [section, in MetaRocq.Common.BasicAst]
ContextMap.f [variable, in MetaRocq.Common.BasicAst]
ContextMap.term [variable, in MetaRocq.Common.BasicAst]
ContextMap.term' [variable, in MetaRocq.Common.BasicAst]
ContextNotConvertibleAnn [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ContextNotConvertibleBody [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ContextNotConvertibleLength [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ContextNotConvertibleType [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ContextReduction [section, in MetaRocq.PCUIC.PCUICContextConversion]
ContextReduction.cf [variable, in MetaRocq.PCUIC.PCUICContextConversion]
ContextReduction.wfΣ [variable, in MetaRocq.PCUIC.PCUICContextConversion]
ContextReduction.Σ [variable, in MetaRocq.PCUIC.PCUICContextConversion]
Contexts [section, in MetaRocq.Common.BasicAst]
Contexts [section, in MetaRocq.Common.BasicAst]
Contexts [section, in MetaRocq.Common.BasicAst]
ContextSet [module, in MetaRocq.Common.Universes]
ContextSet.constraints [definition, in MetaRocq.Common.Universes]
ContextSet.empty [definition, in MetaRocq.Common.Universes]
ContextSet.equal [definition, in MetaRocq.Common.Universes]
ContextSet.Equal [definition, in MetaRocq.Common.Universes]
ContextSet.equal_spec [lemma, in MetaRocq.Common.Universes]
ContextSet.inter [definition, in MetaRocq.Common.Universes]
ContextSet.inter_spec [definition, in MetaRocq.Common.Universes]
ContextSet.is_empty [definition, in MetaRocq.Common.Universes]
ContextSet.levels [definition, in MetaRocq.Common.Universes]
ContextSet.subset [definition, in MetaRocq.Common.Universes]
ContextSet.Subset [definition, in MetaRocq.Common.Universes]
ContextSet.subsetP [lemma, in MetaRocq.Common.Universes]
ContextSet.subset_spec [lemma, in MetaRocq.Common.Universes]
ContextSet.t [definition, in MetaRocq.Common.Universes]
ContextSet.union [definition, in MetaRocq.Common.Universes]
ContextSet.union_spec [definition, in MetaRocq.Common.Universes]
Contexts.term [variable, in MetaRocq.Common.BasicAst]
Contexts.term [variable, in MetaRocq.Common.BasicAst]
Contexts.term [variable, in MetaRocq.Common.BasicAst]
Contexts.term' [variable, in MetaRocq.Common.BasicAst]
Contexts.term' [variable, in MetaRocq.Common.BasicAst]
Contexts.term'' [variable, in MetaRocq.Common.BasicAst]
Contexts.term'' [variable, in MetaRocq.Common.BasicAst]
ContextTest [section, in MetaRocq.Common.BasicAst]
ContextTestK [section, in MetaRocq.Common.BasicAst]
ContextTestK.f [variable, in MetaRocq.Common.BasicAst]
ContextTestK.k [variable, in MetaRocq.Common.BasicAst]
ContextTestK.term [variable, in MetaRocq.Common.BasicAst]
ContextTest.f [variable, in MetaRocq.Common.BasicAst]
ContextTest.term [variable, in MetaRocq.Common.BasicAst]
contextual_closure_red [lemma, in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_sind [definition, in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_rec [definition, in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_ind [definition, in MetaRocq.PCUIC.PCUICReduction]
contextual_closure_rect [definition, in MetaRocq.PCUIC.PCUICReduction]
contextual_closure [inductive, in MetaRocq.PCUIC.PCUICReduction]
context_subst_subst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_app [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_fun' [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_fun [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_length2 [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_assumptions_length [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_length [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_sind [definition, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_rec [definition, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_ind [definition, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_rect [definition, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_def [constructor, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_ass [constructor, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_nil [constructor, in MetaRocq.PCUIC.PCUICContextSubst]
context_subst [inductive, in MetaRocq.PCUIC.PCUICContextSubst]
context_env_clos [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_clos [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_position_valid [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_position_atpos [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_position [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_hole_choice [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_hole_context [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_hole [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_choice_term [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_choice [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_decl_choice [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_assumptions_bound [lemma, in MetaRocq.PCUIC.PCUICSR]
context_assumptions_expand_lets_k_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
context_rel_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
context_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
context_size [definition, in MetaRocq.Examples.tauto]
context_pres_let_bodies_red [lemma, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
context_pres_let_bodies_red1 [lemma, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
context_position_nlctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
context_assumptions_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
context_assumptions_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
context_assumptions_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
context_assumptions_subst_telescope [lemma, in MetaRocq.PCUIC.PCUICSpine]
context_subst_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
context_subst_app_inv [lemma, in MetaRocq.PCUIC.PCUICSpine]
context_to_erased [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
context_conversion [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
context_cumulativity [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
context_cumulativity_prop [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
context_assumptions_expand_lets_ctx [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
context_assumptions_smash_context [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
context_cumulativity_app [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
context_cumulativity_wf_app [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
context_assumptions_lift [lemma, in MetaRocq.Template.EtaExpand]
context_assumptions_lift' [lemma, in MetaRocq.Template.EtaExpand]
context_assumptions_fold_context_k_defs [lemma, in MetaRocq.Template.EtaExpand]
context_assumptions_firstn [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_cumulativity_spec [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_assumptions_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_assumptions_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
context_subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICContexts]
context_subst_lift [lemma, in MetaRocq.PCUIC.PCUICContexts]
context_assumptions_context [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
context_decl [record, in MetaRocq.Common.BasicAst]
context_reflect [instance, in MetaRocq.PCUIC.PCUICAst]
context_assumptions_mapi_context [lemma, in MetaRocq.PCUIC.PCUICAst]
context_depth_inst_case_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
context_depth [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICDepth]
context_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
context_subst_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICInductives]
context_decl [record, in MetaRocq.Erasure.EAst]
context_conversion_cumul_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
context_assumptions_fake_params [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash_context'' [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash_context' [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_fold_context_term [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_cumulativity_wt_decl [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
context_cumulativity_welltyped [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
context_assumptions_map2_set_binder_name [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
context_assumptions_map [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
context_assumptions_map [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Conv [constructor, in MetaRocq.Common.BasicAst]
Conv [constructor, in MetaRocq.Template.Checker]
convAlgo [abbreviation, in MetaRocq.PCUIC.PCUICCumulativity]
ConvCongruences [section, in MetaRocq.PCUIC.PCUICConversion]
ConvCongruences.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvCongruences.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvCongruences.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvError [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion [module, in MetaRocq.Common.EnvironmentTyping]
Conversion [section, in MetaRocq.Template.Checker]
Conversion [section, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionError [inductive, in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_sind [definition, in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_rec [definition, in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_ind [definition, in MetaRocq.SafeChecker.PCUICErrors]
ConversionError_rect [definition, in MetaRocq.SafeChecker.PCUICErrors]
ConversionParSig [module, in MetaRocq.Common.EnvironmentTyping]
ConversionParSig.cumul_gen [axiom, in MetaRocq.Common.EnvironmentTyping]
ConversionResult [inductive, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary [inductive, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_sind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_rec [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_ind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResultSummary_rect [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_sind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_rec [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_ind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionResult_rect [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConversionSig [module, in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_sind [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_rec [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_ind [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb_rect [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.all_decls_alpha_vdef [constructor, in MetaRocq.Common.EnvironmentTyping]
Conversion.all_decls_alpha_vass [constructor, in MetaRocq.Common.EnvironmentTyping]
Conversion.All_decls_alpha_pb [inductive, in MetaRocq.Common.EnvironmentTyping]
Conversion.cf [variable, in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.conv [abbreviation, in MetaRocq.Common.EnvironmentTyping]
Conversion.Conversion [section, in MetaRocq.Common.EnvironmentTyping]
Conversion.Conversion.cumul_gen [variable, in MetaRocq.Common.EnvironmentTyping]
Conversion.conv_context [abbreviation, in MetaRocq.Common.EnvironmentTyping]
Conversion.conv_decls [abbreviation, in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul [abbreviation, in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_context [abbreviation, in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_decls [abbreviation, in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_ctx_rel [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_pb_context [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.cumul_pb_decls [definition, in MetaRocq.Common.EnvironmentTyping]
Conversion.flags [variable, in MetaRocq.Template.Checker]
Conversion.G [variable, in MetaRocq.Template.Checker]
Conversion.nor [variable, in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.normalization_in [variable, in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.X [variable, in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.X_type [variable, in MetaRocq.SafeChecker.PCUICSafeConversion]
Conversion.Σ [variable, in MetaRocq.Template.Checker]
convert [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
convert_leq [definition, in MetaRocq.Template.Checker]
ConvRedConv [section, in MetaRocq.PCUIC.PCUICConversion]
ConvRedConv.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvRedConv.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvRedConv.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
convSpec [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
convSpec_renameP [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
convSpec_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
convSpec_convAlgo_curry [lemma, in MetaRocq.PCUIC.PCUICConversion]
convSpec_convAlgo [lemma, in MetaRocq.PCUIC.PCUICConversion]
convSpec_cumulSpec [lemma, in MetaRocq.PCUIC.PCUICConversion]
convSpec0_ind_all [lemma, in MetaRocq.PCUIC.PCUICCumulativitySpec]
ConvSubst [section, in MetaRocq.PCUIC.PCUICConversion]
ConvSubst.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvSubst.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvSubst.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvSuccess [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
ConvTerms [section, in MetaRocq.PCUIC.PCUICConversion]
ConvTerms.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvTerms.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
ConvTerms.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
conv_ar [projection, in MetaRocq.Erasure.Typed.Erasure]
conv_arity_Is_conv_to_Arity [lemma, in MetaRocq.Erasure.Typed.Erasure]
conv_arity_or_not [definition, in MetaRocq.Erasure.Typed.Erasure]
conv_ar_red [projection, in MetaRocq.Erasure.Typed.Erasure]
conv_ar_univ [projection, in MetaRocq.Erasure.Typed.Erasure]
conv_ar_context [projection, in MetaRocq.Erasure.Typed.Erasure]
conv_arity [record, in MetaRocq.Erasure.Typed.Erasure]
conv_ctx_refl' [definition, in MetaRocq.PCUIC.PCUICCumulativity]
conv_ctx_refl [instance, in MetaRocq.PCUIC.PCUICCumulativity]
conv_context [abbreviation, in MetaRocq.PCUIC.PCUICCumulativity]
conv_sym [instance, in MetaRocq.PCUIC.PCUICCumulativity]
conv_cumul_inv [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
conv_cumul [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
conv_cumul2 [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
conv_refl' [instance, in MetaRocq.PCUIC.PCUICCumulativity]
conv_decls_refl [instance, in MetaRocq.PCUIC.PCUICCumulativity]
conv_ctx_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICSR]
conv_context_refl [instance, in MetaRocq.PCUIC.PCUICSR]
conv_refl' [lemma, in MetaRocq.PCUIC.PCUICSR]
conv_context_rel_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICSR]
conv_context_rel_reln [lemma, in MetaRocq.PCUIC.PCUICSR]
conv_context_smash_end [lemma, in MetaRocq.PCUIC.PCUICSR]
conv_context_app [lemma, in MetaRocq.Erasure.Prelim]
conv_vdef_body [constructor, in MetaRocq.Erasure.Prelim]
conv_vdef_type [constructor, in MetaRocq.Erasure.Prelim]
conv_vass [constructor, in MetaRocq.Erasure.Prelim]
conv_arity_Is_conv_to_Arity [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
conv_ar_red [projection, in MetaRocq.SafeChecker.PCUICSafeReduce]
conv_ar_univ [projection, in MetaRocq.SafeChecker.PCUICSafeReduce]
conv_ar_context [projection, in MetaRocq.SafeChecker.PCUICSafeReduce]
conv_arity [record, in MetaRocq.SafeChecker.PCUICSafeReduce]
conv_cum_zipp [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
conv_alt_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
conv_alt_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
conv_cum [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
conv_trans [instance, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
conv_pb_relb_gen [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
conv_context_wf_local_app [lemma, in MetaRocq.Erasure.ErasureProperties]
conv_context_app_same [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_cumul_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_context_sym [instance, in MetaRocq.PCUIC.PCUICContextConversion]
conv_alt_red_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_alt_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_leq_context_upto_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_leq_context_upto [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_eq_context_upto [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
conv_context [abbreviation, in MetaRocq.PCUIC.PCUICContextConversion]
conv_decorate_hetero [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
conv_decorate [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
conv_ctx_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
conv_decls_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
conv_betas_typed [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_decls_fix_context [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_decls_fix_context_gen [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_eq_ctx [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_betas [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_inds [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_Lambda [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_conv_iff [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_iff [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_conv_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_conv [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_cum_conv_ctx [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_red_conv [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_Prod_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
conv_renameP [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
conv_context_smash [lemma, in MetaRocq.PCUIC.PCUICContexts]
conv_pb_leqb [definition, in MetaRocq.Common.BasicAst]
conv_pb_sind [definition, in MetaRocq.Common.BasicAst]
conv_pb_rec [definition, in MetaRocq.Common.BasicAst]
conv_pb_ind [definition, in MetaRocq.Common.BasicAst]
conv_pb_rect [definition, in MetaRocq.Common.BasicAst]
conv_pb [inductive, in MetaRocq.Common.BasicAst]
conv_ctx_refl' [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_ctx_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_context [abbreviation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_decls_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_refl' [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_refl' [lemma, in MetaRocq.Template.Typing]
conv_pb_sind [definition, in MetaRocq.Template.Checker]
conv_pb_rec [definition, in MetaRocq.Template.Checker]
conv_pb_ind [definition, in MetaRocq.Template.Checker]
conv_pb_rect [definition, in MetaRocq.Template.Checker]
conv_pb [inductive, in MetaRocq.Template.Checker]
conv_lift_judgment_univ [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_lift_judgment [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_ind [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_prod [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_sort [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_check [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_ctx_prop_app [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
conv_ctx_prop_refl [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
conv_ctx_prop [abbreviation, in MetaRocq.PCUIC.PCUICCumulProp]
conv_decls_prop [definition, in MetaRocq.PCUIC.PCUICCumulProp]
conv_sort_inv [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
conv_cum_tProj_inv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_tCoFix_inv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_tFix_inv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_tCase_inv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_napp [definition, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_conv_cum_r [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_conv_cum_l [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_alt [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum [definition, in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_to_arity_cumul [lemma, in MetaRocq.Erasure.EArities]
conv_cum_red_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_cum_red_conv_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_context_decl [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_term [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_stack_ctx [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_cum_trans [instance, in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_decls_irrel_sec [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
conv_pb_relb_gen_proper [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
Core [library]
Core [library]
cored [inductive, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_prod_r [lemma, in MetaRocq.Erasure.Typed.Erasure]
cored_prod_l [lemma, in MetaRocq.Erasure.Typed.Erasure]
cored_welltyped [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
cored_zipc [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_red_cored [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_const [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_red [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_proj [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_case [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_red_trans [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_trans' [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_welltyped [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_sind [definition, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_ind [definition, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_trans [constructor, in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_extends [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
cored_cored' [lemma, in MetaRocq.PCUIC.PCUICSN]
cored_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICSN]
cored_upto [lemma, in MetaRocq.PCUIC.PCUICSN]
cored_alt [lemma, in MetaRocq.PCUIC.PCUICSN]
cored_redp [lemma, in MetaRocq.SafeChecker.PCUICWfReduction]
cored_transitive [instance, in MetaRocq.SafeChecker.PCUICWfReduction]
cored' [definition, in MetaRocq.PCUIC.PCUICSN]
cored'_postpone [lemma, in MetaRocq.PCUIC.PCUICSN]
cored1 [constructor, in MetaRocq.PCUIC.PCUICSafeLemmata]
CorrectDecl [constructor, in MetaRocq.SafeChecker.PCUICErrors]
CorrectDecl [constructor, in MetaRocq.Template.Checker]
CorrectExtractTransform [definition, in MetaRocq.Erasure.Typed.Transform]
correct_valuation_of_labelling_satisfies [lemma, in MetaRocq.Common.uGraph]
correct_labelling_of_valuation_satisfies_iff [lemma, in MetaRocq.Common.uGraph]
correct_labelling_proper [instance, in MetaRocq.Common.uGraph]
CounterModel [constructor, in MetaRocq.Examples.tauto]
count_ones [definition, in MetaRocq.Erasure.Typed.Optimize]
count_zeros [definition, in MetaRocq.Erasure.Typed.Optimize]
count_zeros_nth_error [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_ones_zeros [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_distr_app [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_repeat [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_rev [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_le [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
creflexive_eq [instance, in MetaRocq.PCUIC.PCUICEquality]
CS [module, in MetaRocq.Common.Universes]
csort_sup_mon [lemma, in MetaRocq.Common.Universes]
csort_sup_not_uproplevel [lemma, in MetaRocq.Common.Universes]
csort_sup_comm [lemma, in MetaRocq.Common.Universes]
cstr_arity [definition, in MetaRocq.Template.WcbvEval]
cstr_branch_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICProgress]
cstr_arity [definition, in MetaRocq.Erasure.EAst]
cstr_nargs [projection, in MetaRocq.Erasure.EAst]
cstr_name [projection, in MetaRocq.Erasure.EAst]
cstr_as_blocks [projection, in MetaRocq.Erasure.EWellformed]
cstr_branch_context_length [lemma, in MetaRocq.Template.TypingWf]
cstr_branch_context_assumptions [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
cstr_branch_context_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
cstr_branch_context [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
cstr_branch_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
cstr_arity [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
cstr_branch_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
cstr_branch_context [definition, in MetaRocq.Template.Ast]
cstr_indices_length [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
cst_body [projection, in MetaRocq.Erasure.Typed.ExAst]
cst_type [projection, in MetaRocq.Erasure.Typed.ExAst]
cst_body [projection, in MetaRocq.Erasure.EAst]
csubst [definition, in MetaRocq.Erasure.ECSubst]
csubst [definition, in MetaRocq.Template.WcbvEval]
csubst [definition, in MetaRocq.PCUIC.PCUICCSubst]
csubst_closed [lemma, in MetaRocq.Erasure.ECSubst]
csubst_mkApps [lemma, in MetaRocq.Erasure.ECSubst]
csubst_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
csubst_mkApps [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
csubst_closed [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
csubst_mkApps [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
csubst_closed [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
csubst_mkApps [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
CS_For_all_proper [instance, in MetaRocq.Common.Universes]
CS_For_all_add [lemma, in MetaRocq.Common.Universes]
CS_For_all_union [lemma, in MetaRocq.Common.Universes]
CS_union_empty [lemma, in MetaRocq.Common.Universes]
cs_equal [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
ctors_info [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
ctor_masks [projection, in MetaRocq.Erasure.Typed.Optimize]
ctxclos_ctx [constructor, in MetaRocq.PCUIC.PCUICReduction]
ctxclos_atom [constructor, in MetaRocq.PCUIC.PCUICReduction]
CtxInstSize [section, in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize [section, in MetaRocq.Template.Typing]
CtxInstSize.cf [variable, in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize.typing [variable, in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize.typing [variable, in MetaRocq.Template.Typing]
CtxInstSize.typing_size [variable, in MetaRocq.PCUIC.PCUICTyping]
CtxInstSize.typing_size [variable, in MetaRocq.Template.Typing]
ctxmap [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_fix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_cofix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_ext [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
CtxReduction [section, in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction [section, in MetaRocq.PCUIC.PCUICContextReduction]
CtxReduction.cf [variable, in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction.cf [variable, in MetaRocq.PCUIC.PCUICContextReduction]
CtxReduction.wfΣ [variable, in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction.wfΣ [variable, in MetaRocq.PCUIC.PCUICContextReduction]
CtxReduction.Σ [variable, in MetaRocq.PCUIC.PCUICSubstitution]
CtxReduction.Σ [variable, in MetaRocq.PCUIC.PCUICContextReduction]
ctx_inst_merge' [lemma, in MetaRocq.PCUIC.PCUICSR]
ctx_inst_merge [lemma, in MetaRocq.PCUIC.PCUICSR]
ctx_inst_eq_context [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_open_terms [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_smash [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_smash_acc [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_cumul [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_spine_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_ass [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_def [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_app_sub [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_eq [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_app_inv [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_subst_length [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_spec [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub [definition, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_weaken [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_length [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst [abbreviation, in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_size [definition, in MetaRocq.PCUIC.PCUICTyping]
ctx_inst_on_universes [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
ctx_inst_wt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ctx_inst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ctx_inst_bd_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
ctx_inst_impl [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
ctx_inst_app_weak [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ctx_inst_eq_context [lemma, in MetaRocq.PCUIC.PCUICAlpha]
ctx_length_rev_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
ctx_length_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
ctx_inst_wt [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
ctx_inst_smash [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
ctx_inst_size [definition, in MetaRocq.Template.Typing]
ctx_inst_typing_bd [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_app_impl [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_length [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_wt [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
ctx_inst_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
Cumul [constructor, in MetaRocq.Common.BasicAst]
Cumul [constructor, in MetaRocq.Template.Checker]
cumulAlgo [abbreviation, in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_sind [definition, in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_rec [definition, in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_ind [definition, in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen_rect [definition, in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_gen [inductive, in MetaRocq.PCUIC.PCUICCumulativity]
cumulAlgo_cumulSpec [lemma, in MetaRocq.PCUIC.PCUICConversion]
cumulP [inductive, in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_sind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_rec [definition, in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_ind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
cumulP_rect [definition, in MetaRocq.PCUIC.PCUICSubstitution]
cumulSpec [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
CumulSpecIsCumulAlgo [section, in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo [section, in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
CumulSpecIsCumulAlgo.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
cumulSpec_renameP [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
cumulSpec_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cumulSpec_typed_cumulAlgo [lemma, in MetaRocq.PCUIC.PCUICConversion]
cumulSpec_cumulAlgo_curry [lemma, in MetaRocq.PCUIC.PCUICConversion]
cumulSpec_cumulAlgo [lemma, in MetaRocq.PCUIC.PCUICConversion]
cumulSpec0 [inductive, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumulSpec0_ind [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumulSpec0_rec [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumulSpec0_ind_all [abbreviation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumulSpec0_rect [lemma, in MetaRocq.PCUIC.PCUICCumulativitySpec]
CumulSubst [section, in MetaRocq.PCUIC.PCUICConversion]
CumulSubst.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
CumulSubst.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
CumulSubst.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
cumul_ctx_refl' [definition, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_ctx_refl [instance, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_context [abbreviation, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_App_l [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_refl' [instance, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_alt [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_decls_refl [instance, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_pb_decls_refl [instance, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_red_r [constructor, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_red_l [constructor, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_refl [constructor, in MetaRocq.PCUIC.PCUICCumulativity]
cumul_Sort_Prod_discr [lemma, in MetaRocq.Erasure.Prelim]
cumul_sprop2 [lemma, in MetaRocq.PCUIC.PCUICElimination]
cumul_sprop1 [lemma, in MetaRocq.PCUIC.PCUICElimination]
cumul_prop2 [lemma, in MetaRocq.PCUIC.PCUICElimination]
cumul_prop1 [lemma, in MetaRocq.PCUIC.PCUICElimination]
cumul_prop_inv [lemma, in MetaRocq.PCUIC.PCUICElimination]
cumul_trans [instance, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
cumul_context_Algo_Spec [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
cumul_context_app_same [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_alt_red_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_alt_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_alt_red_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_alt_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_eq_context_upto [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_leq_context_upto [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_compare_context_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_compare_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_trans_red_leqterm [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_red_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_context [abbreviation, in MetaRocq.PCUIC.PCUICContextConversion]
cumul_decorate_hetero [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_type_irrelevance [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_context_Spec_Algo [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_decorate [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_decls_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cumul_ctx_relSpec_Algo [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
cumul_Prod_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
cumul_mkApps [lemma, in MetaRocq.PCUIC.PCUICConversion]
cumul_renameP [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
cumul_ctx_refl' [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_ctx_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_pb_ctx_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_context [abbreviation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_decls_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_pb_decls_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_spec_refl [instance, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_proj [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_delta [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_cofix_proj [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_cofix_case [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_fix [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_iota [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_rel [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_zeta [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_beta [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Prim [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_CoFix [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Fix [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Proj [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Case [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_LetIn [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Prod [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Lambda [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_App [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Evar [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Const [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Sort [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Construct [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Ind [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Refl [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Sym [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Trans [constructor, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Construct_univ [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_Ind_univ [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_mfixpoint [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_branches [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_branch [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_predicate_undep [lemma, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_predicate_dep [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_predicate [definition, in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_ctx_rel_close' [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
cumul_decl [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
cumul_refl' [lemma, in MetaRocq.Template.Typing]
cumul_gen_sind [definition, in MetaRocq.Template.Typing]
cumul_gen_rec [definition, in MetaRocq.Template.Typing]
cumul_gen_ind [definition, in MetaRocq.Template.Typing]
cumul_gen_rect [definition, in MetaRocq.Template.Typing]
cumul_red_r [constructor, in MetaRocq.Template.Typing]
cumul_red_l [constructor, in MetaRocq.Template.Typing]
cumul_refl [constructor, in MetaRocq.Template.Typing]
cumul_gen [inductive, in MetaRocq.Template.Typing]
cumul_prop_is_open [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_sym' [instance, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_mkApps_Ind_inv [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_mkApps [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_tLetIn [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_tProd [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_subst_instance [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_args [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_prod_inv [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_cum_pb_r [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_cumul_pb_l [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_transitive [instance, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_trans [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_sym [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_sprop_props [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_props [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_sort [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_alt [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_pb_cumul_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_sind [definition, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_rec [definition, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_ind [definition, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_rect [definition, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_red_r [constructor, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_red_l [constructor, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_refl [constructor, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop [inductive, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_ind_confluence [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_sort_confluence [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
cumul_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICClassification]
cumul_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cumul_prop2' [lemma, in MetaRocq.Erasure.EArities]
cumul_prop1' [lemma, in MetaRocq.Erasure.EArities]
cumul_propositional [lemma, in MetaRocq.Erasure.EArities]
cumul_sprop2 [lemma, in MetaRocq.Erasure.EArities]
cumul_sprop1 [lemma, in MetaRocq.Erasure.EArities]
cumul_prop2 [lemma, in MetaRocq.Erasure.EArities]
cumul_prop1 [lemma, in MetaRocq.Erasure.EArities]
cumul_ctx_rel_cons [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
cumul_decls_irrel_sec [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
cumul_decorate [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
cunfold_cofix [definition, in MetaRocq.Template.WcbvEval]
cunfold_fix [definition, in MetaRocq.Template.WcbvEval]
cunfold_cofix [definition, in MetaRocq.Erasure.EGlobalEnv]
cunfold_fix [definition, in MetaRocq.Erasure.EGlobalEnv]
cunfold_cofix [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
cunfold_fix [definition, 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) |