| 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) |
N
name [inductive, in MetaRocq.Common.BasicAst]named_extraction_env_flags [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
named_extraction_term_flags [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
nameless [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nameless_eq_term_spec [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nameless_eqctx_IH [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nameless_ctx [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nameless_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
name_from_term [definition, in MetaRocq.Template.Pretty]
name_from_term [definition, in MetaRocq.PCUIC.utils.PCUICPretty]
name_sind [definition, in MetaRocq.Common.BasicAst]
name_rec [definition, in MetaRocq.Common.BasicAst]
name_ind [definition, in MetaRocq.Common.BasicAst]
name_rect [definition, in MetaRocq.Common.BasicAst]
name_from_term [definition, in MetaRocq.Erasure.EPretty]
nAnon [constructor, in MetaRocq.Common.BasicAst]
nApp [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nApp_mkApps [lemma, in MetaRocq.Template.AstUtils]
nApp_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
nApp_isApp_false [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
nApp_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
nApp_decompose_app [lemma, in MetaRocq.Erasure.EAstUtils]
NativeCast [constructor, in MetaRocq.Common.BasicAst]
nat_show [instance, in MetaRocq.Utils.Show]
nat_le_irrel [lemma, in MetaRocq.Common.Reflect]
nat_recursion_ext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
nat_rev_ind [lemma, in MetaRocq.Utils.MRArith]
Nat_module [abbreviation, in MetaRocq.Examples.demo]
Nbar [module, in MetaRocq.Utils.wGraph]
Nbar_max_le [lemma, in MetaRocq.Common.uGraph]
Nbar_max_spec'' [lemma, in MetaRocq.Common.uGraph]
Nbar_max_spec' [lemma, in MetaRocq.Common.uGraph]
Nbar_max_spec [lemma, in MetaRocq.Common.uGraph]
Nbar.add [definition, in MetaRocq.Utils.wGraph]
Nbar.add_max_distr_r [definition, in MetaRocq.Utils.wGraph]
Nbar.add_0_l [lemma, in MetaRocq.Utils.wGraph]
Nbar.add_0_r [definition, in MetaRocq.Utils.wGraph]
Nbar.add_assoc [definition, in MetaRocq.Utils.wGraph]
Nbar.add_finite [lemma, in MetaRocq.Utils.wGraph]
Nbar.eq_max [lemma, in MetaRocq.Utils.wGraph]
Nbar.fold_max_le' [lemma, in MetaRocq.Utils.wGraph]
Nbar.fold_max_le [lemma, in MetaRocq.Utils.wGraph]
Nbar.fold_max_In [lemma, in MetaRocq.Utils.wGraph]
Nbar.le [definition, in MetaRocq.Utils.wGraph]
Nbar.le_antisymm [lemma, in MetaRocq.Utils.wGraph]
Nbar.le_plus_r [lemma, in MetaRocq.Utils.wGraph]
Nbar.le_lt_dec [lemma, in MetaRocq.Utils.wGraph]
Nbar.le_dec [lemma, in MetaRocq.Utils.wGraph]
Nbar.le_trans [instance, in MetaRocq.Utils.wGraph]
Nbar.le_refl [instance, in MetaRocq.Utils.wGraph]
Nbar.lt [definition, in MetaRocq.Utils.wGraph]
Nbar.max [definition, in MetaRocq.Utils.wGraph]
Nbar.max_idempotent [definition, in MetaRocq.Utils.wGraph]
Nbar.max_le' [definition, in MetaRocq.Utils.wGraph]
Nbar.max_lub [definition, in MetaRocq.Utils.wGraph]
Nbar.max_None [lemma, in MetaRocq.Utils.wGraph]
Nbar.plus_le_compat [definition, in MetaRocq.Utils.wGraph]
Nbar.plus_le_compat_l [definition, in MetaRocq.Utils.wGraph]
Nbar.S [definition, in MetaRocq.Utils.wGraph]
Nbar.sub [definition, in MetaRocq.Utils.wGraph]
Nbar.sub_diag [lemma, in MetaRocq.Utils.wGraph]
Nbar.t [definition, in MetaRocq.Utils.wGraph]
_ < _ (nbar_scope) [notation, in MetaRocq.Utils.wGraph]
_ <= _ (nbar_scope) [notation, in MetaRocq.Utils.wGraph]
_ - _ (nbar_scope) [notation, in MetaRocq.Utils.wGraph]
_ + _ (nbar_scope) [notation, in MetaRocq.Utils.wGraph]
nclosed_represents [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
ne [inductive, in MetaRocq.PCUIC.PCUICNormal]
negb_is_true [lemma, in MetaRocq.PCUIC.PCUICNormal]
negb_False [lemma, in MetaRocq.PCUIC.PCUICClassification]
neg_pb_of_dec [definition, in MetaRocq.Quotation.CommonUtils]
neg_bp_of_dec [definition, in MetaRocq.Quotation.CommonUtils]
neg_forall [definition, in MetaRocq.Common.uGraph]
neqb [lemma, in MetaRocq.Utils.ReflectEq]
neutral [inductive, in MetaRocq.Template.Normal]
neutral_sind [definition, in MetaRocq.Template.Normal]
neutral_ind [definition, in MetaRocq.Template.Normal]
neval_to_stuck_fix_app [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
neval_to_stuck_fix [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
new_cstr [definition, in MetaRocq.Examples.add_constructor]
new_var [definition, in MetaRocq.Erasure.Typed.Optimize]
new_vars [definition, in MetaRocq.Erasure.Typed.Optimize]
new_tag_spec [lemma, in MetaRocq.Erasure.EReorderCstrs]
new_tag [definition, in MetaRocq.Erasure.EReorderCstrs]
ne_nisConstruct_app [lemma, in MetaRocq.PCUIC.PCUICNormal]
ne_tCoFix_app [lemma, in MetaRocq.PCUIC.PCUICNormal]
ne_tConstruct_app [lemma, in MetaRocq.PCUIC.PCUICNormal]
ne_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
ne_nf_ind_all [lemma, in MetaRocq.PCUIC.PCUICNormal]
ne_ind_all [lemma, in MetaRocq.PCUIC.PCUICNormal]
ne_nf_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
ne_sind [definition, in MetaRocq.PCUIC.PCUICNormal]
ne_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
ne_nf [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_proj [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_case [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_fixapp [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_const [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_app [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_evar [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_var [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_rel [constructor, in MetaRocq.PCUIC.PCUICNormal]
ne_proj [constructor, in MetaRocq.Template.Normal]
ne_case [constructor, in MetaRocq.Template.Normal]
ne_app [constructor, in MetaRocq.Template.Normal]
ne_const [constructor, in MetaRocq.Template.Normal]
ne_evar [constructor, in MetaRocq.Template.Normal]
ne_var [constructor, in MetaRocq.Template.Normal]
ne_rel [constructor, in MetaRocq.Template.Normal]
ne_nf_smash_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
nf [inductive, in MetaRocq.PCUIC.PCUICNormal]
nf_red [lemma, in MetaRocq.PCUIC.PCUICNormal]
nf_no_red [lemma, in MetaRocq.PCUIC.PCUICNormal]
nf_ind_all [lemma, in MetaRocq.PCUIC.PCUICNormal]
nf_ne_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
nf_sind [definition, in MetaRocq.PCUIC.PCUICNormal]
nf_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
nf_tProd [constructor, in MetaRocq.PCUIC.PCUICNormal]
nf_tind [constructor, in MetaRocq.PCUIC.PCUICNormal]
nf_cofix [constructor, in MetaRocq.PCUIC.PCUICNormal]
nf_construct [constructor, in MetaRocq.PCUIC.PCUICNormal]
nf_lam [constructor, in MetaRocq.PCUIC.PCUICNormal]
nf_cofix [constructor, in MetaRocq.Template.Normal]
nf_fix [constructor, in MetaRocq.Template.Normal]
nf_indapp [constructor, in MetaRocq.Template.Normal]
nf_cstrapp [constructor, in MetaRocq.Template.Normal]
nf_lam [constructor, in MetaRocq.Template.Normal]
nf_prod [constructor, in MetaRocq.Template.Normal]
nf_sort [constructor, in MetaRocq.Template.Normal]
nf_ne [constructor, in MetaRocq.Template.Normal]
nil_prefix [lemma, in MetaRocq.Utils.MRList]
nisApp_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nisArityHead_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
nisBox_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
nisErasable [definition, in MetaRocq.Erasure.Extract]
nisErasable_lets [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
nisErasable_eval [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
nisErasable_spec [lemma, in MetaRocq.Erasure.Extract]
nisErasable_tPrim [lemma, in MetaRocq.Erasure.EArities]
nisErasable_Propositional [lemma, in MetaRocq.Erasure.EArities]
nisFixApp_nisFix [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
nisFix_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
nisLambda_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
nisLambda_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
nisLazy_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
nisPrim_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
nisPrim_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
nIs_conv_to_Arity_isWfArity_elim [lemma, in MetaRocq.Erasure.EArities]
nIs_conv_to_Arity_nArity [lemma, in MetaRocq.Erasure.EArities]
nl [definition, in MetaRocq.Utils.MRString]
nl [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nlctx [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nlctx_smash_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_binders [definition, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_length [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_lift_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_subst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_fix_context_alt [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_app_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_spec [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nldecl [abbreviation, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nlg [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nlict [definition, in MetaRocq.PCUIC.PCUICAst]
nl_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_is_allowed_elimination [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_global_ext_levels [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_global_levels [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_red1 [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_branches [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_branch [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_predicate [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_forget_types [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_branch_type [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_branch_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_cstr_branch_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_predicate_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_inst_case_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_inds [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_lift_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_telescope [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets_k [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_extended_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_to_extended_list [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_declared_constructor [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_declared_inductive [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_fix_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_pred_set_pparams [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_pred_set_preturn [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_decompose_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_decl' [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_decl [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_mkApps [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_decompose_prod_assum [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_compare_term [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_term [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_leq_term [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_term_upto_univ [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_context_assumptions [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_destArity [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_lookup_env [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_spec [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
nl_mfix [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
nl_global_env [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_global_declarations [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_global_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_mutual_inductive_body [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_one_inductive_body [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_projection_body [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_constructor_body [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_constant_body [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_branch [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nl_predicate [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
nNamed [constructor, in MetaRocq.Common.BasicAst]
no [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
noccur_between [definition, in MetaRocq.PCUIC.PCUICAst]
noccur_shift [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
noccur_between [definition, in MetaRocq.Template.Ast]
nocc_between [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
nocc_betweenp [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
NoConfusion_byte_alt [definition, in MetaRocq.Utils.ByteCompareSpec]
nodelta_flags [definition, in MetaRocq.Template.Checker]
NoDup_In_1 [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
NoDup_gen_many_fresh [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
NoDup_map [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
NoDup_extends [lemma, in MetaRocq.Template.TypingWf]
nonEmptyLevelExprSet [record, in MetaRocq.Common.Universes]
NonEmptySetFacts [module, in MetaRocq.Common.Universes]
NonEmptySetFacts.add [definition, in MetaRocq.Common.Universes]
NonEmptySetFacts.add_list_spec [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.add_list [definition, in MetaRocq.Common.Universes]
NonEmptySetFacts.add_spec [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.elements_not_empty [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.eq_univ'' [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.eq_univ' [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.eq_univ [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.In_to_nonempty_list_rev [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.In_to_nonempty_list [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.LevelExprSet_For_all_exprs [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.LevelExprSet_for_all_false [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.map [definition, in MetaRocq.Common.Universes]
NonEmptySetFacts.map_spec [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.non_empty_union [definition, in MetaRocq.Common.Universes]
NonEmptySetFacts.not_Empty_is_empty [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.singleton [definition, in MetaRocq.Common.Universes]
NonEmptySetFacts.singleton_to_nonempty_list [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.to_nonempty_list_spec' [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.to_nonempty_list_spec [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.to_nonempty_list [definition, in MetaRocq.Common.Universes]
NonEmptySetFacts.univ_expr_eqb_comm [lemma, in MetaRocq.Common.Universes]
NonEmptySetFacts.univ_expr_eqb_true_iff [lemma, in MetaRocq.Common.Universes]
NonRec [inductive, in MetaRocq.Examples.demo]
NonRec_sind [definition, in MetaRocq.Examples.demo]
NonRec_rec [definition, in MetaRocq.Examples.demo]
NonRec_ind [definition, in MetaRocq.Examples.demo]
NonRec_rect [definition, in MetaRocq.Examples.demo]
Normal [section, in MetaRocq.PCUIC.PCUICNormal]
Normal [section, in MetaRocq.PCUIC.PCUICNormal]
normal [inductive, in MetaRocq.Template.Normal]
Normal [section, in MetaRocq.Template.Normal]
Normal [library]
normalization [projection, in MetaRocq.PCUIC.PCUICSN]
Normalization [record, in MetaRocq.PCUIC.PCUICSN]
normalization [constructor, in MetaRocq.PCUIC.PCUICSN]
Normalization [inductive, in MetaRocq.PCUIC.PCUICSN]
NormalizationIn [record, in MetaRocq.PCUIC.PCUICSN]
NormalizationIn [inductive, in MetaRocq.PCUIC.PCUICSN]
normalizationInAdjustUniversesIn [record, in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
normalizationInAdjustUniversesIn [inductive, in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
NormalizationIn_erase_global_deps [abbreviation, in MetaRocq.Erasure.ErasureFunction]
NormalizationIn_erase_global_deps_fast [abbreviation, in MetaRocq.Erasure.ErasureFunctionProperties]
NormalizationIn_erase_pcuic_program_2 [abbreviation, in MetaRocq.ErasurePlugin.ETransform]
NormalizationIn_erase_pcuic_program_1 [abbreviation, in MetaRocq.ErasurePlugin.ETransform]
normalization_in_adjust_universes [projection, in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
normalization_in_adjust_universes [constructor, in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
normalization_in_inv [lemma, in MetaRocq.Erasure.ErasureFunction]
normalization_in_extends [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
normalization_upto [lemma, in MetaRocq.PCUIC.PCUICSN]
normalization_in [projection, in MetaRocq.PCUIC.PCUICSN]
normalization_in [constructor, in MetaRocq.PCUIC.PCUICSN]
normalizing_flags [record, in MetaRocq.PCUIC.PCUICSN]
normal_sind [definition, in MetaRocq.Template.Normal]
normal_ind [definition, in MetaRocq.Template.Normal]
Normal.flags [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.flags [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hprod [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hind [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hcofix [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hconstruct [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hlam [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hne [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hproj [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hcase [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hfix [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hcst [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.happ [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hevar [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hvar [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.hrel [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.P0 [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind.P [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.nf_ne_ind [section, in MetaRocq.PCUIC.PCUICNormal]
Normal.Σ [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.Σ [variable, in MetaRocq.PCUIC.PCUICNormal]
Normal.Σ [variable, in MetaRocq.Template.Normal]
nor_check_univs [projection, in MetaRocq.PCUIC.PCUICSN]
not [definition, in MetaRocq.Examples.tauto]
NotAnArity [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotAnInductive [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotAnInductive [constructor, in MetaRocq.Template.Checker]
NotAProduct [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotAProduct [constructor, in MetaRocq.Template.Checker]
NotASort [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotASort [constructor, in MetaRocq.Template.Checker]
notCoInductive [definition, in MetaRocq.PCUIC.PCUICClassification]
NotConvertible [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotConvertible [constructor, in MetaRocq.Template.Checker]
NotCumulSmaller [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotEnoughFuel [constructor, in MetaRocq.Template.Checker]
NotFoundConstant [constructor, in MetaRocq.SafeChecker.PCUICErrors]
NotFoundConstants [constructor, in MetaRocq.SafeChecker.PCUICErrors]
notSolvable [constructor, in MetaRocq.Examples.tauto]
NotSolvable [inductive, in MetaRocq.Examples.tauto]
NotSolvable_sind [definition, in MetaRocq.Examples.tauto]
NotSolvable_rec [definition, in MetaRocq.Examples.tauto]
NotSolvable_ind [definition, in MetaRocq.Examples.tauto]
NotSolvable_rect [definition, in MetaRocq.Examples.tauto]
NotSupported [constructor, in MetaRocq.Template.Checker]
not_prod_or_sort_hnf [lemma, in MetaRocq.Erasure.Typed.Erasure]
not_empty_map [lemma, in MetaRocq.Utils.MRList]
not_var_global_ext_levels [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
not_var_global_levels [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
not_isErasable [lemma, in MetaRocq.Erasure.EArities]
no_prop_leq_type.Hcf [variable, in MetaRocq.PCUIC.PCUICElimination]
no_prop_leq_type.cf [variable, in MetaRocq.PCUIC.PCUICElimination]
no_prop_leq_type [section, in MetaRocq.PCUIC.PCUICElimination]
no_prop_leq_type.ϕ [variable, in MetaRocq.Common.Universes]
no_prop_leq_type.cf [variable, in MetaRocq.Common.Universes]
no_prop_leq_type [section, in MetaRocq.Common.Universes]
no_unsafe_passes [definition, in MetaRocq.ErasurePlugin.Erasure]
_ ;;; _ |- _ ~~ _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulProp]
no_prop_leq_type.Hcf [variable, in MetaRocq.PCUIC.PCUICCumulProp]
no_prop_leq_type.cf [variable, in MetaRocq.PCUIC.PCUICCumulProp]
no_prop_leq_type [section, in MetaRocq.PCUIC.PCUICCumulProp]
no_use_subst [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
nth_error_list_size [lemma, in MetaRocq.Examples.tauto]
nth_error_app_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_appP [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_rect [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_out [constructor, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_right [constructor, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_left [constructor, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec [inductive, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_extended_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_lift_context_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_lift_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_firstn [lemma, in MetaRocq.Utils.MRList]
nth_nth_error' [lemma, in MetaRocq.Utils.MRList]
nth_nth_error [lemma, in MetaRocq.Utils.MRList]
nth_error_unfold_inv [lemma, in MetaRocq.Utils.MRList]
nth_error_unfold [lemma, in MetaRocq.Utils.MRList]
nth_error_snoc [lemma, in MetaRocq.Utils.MRList]
nth_error_rev_inv [lemma, in MetaRocq.Utils.MRList]
nth_error_rev [lemma, in MetaRocq.Utils.MRList]
nth_error_app_inv [lemma, in MetaRocq.Utils.MRList]
nth_error_app_lt [lemma, in MetaRocq.Utils.MRList]
nth_error_app_ge [lemma, in MetaRocq.Utils.MRList]
nth_error_skipn [lemma, in MetaRocq.Utils.MRList]
nth_error_removelast [lemma, in MetaRocq.Utils.MRList]
nth_error_skipn_add [lemma, in MetaRocq.Utils.MRList]
nth_map' [lemma, in MetaRocq.Utils.MRList]
nth_error_nil [lemma, in MetaRocq.Utils.MRList]
nth_error_app_left [lemma, in MetaRocq.Utils.MRList]
nth_error_spec [lemma, in MetaRocq.Utils.MRList]
nth_error_Some' [lemma, in MetaRocq.Utils.MRList]
nth_error_Some_non_nil [lemma, in MetaRocq.Utils.MRList]
nth_error_Some_length [lemma, in MetaRocq.Utils.MRList]
nth_error_mapi [lemma, in MetaRocq.Utils.MRList]
nth_error_mapi_rec [lemma, in MetaRocq.Utils.MRList]
nth_error_Spec_sind [definition, in MetaRocq.Utils.MRList]
nth_error_Spec_rec [definition, in MetaRocq.Utils.MRList]
nth_error_Spec_ind [definition, in MetaRocq.Utils.MRList]
nth_error_Spec_rect [definition, in MetaRocq.Utils.MRList]
nth_error_Spec_None [constructor, in MetaRocq.Utils.MRList]
nth_error_Spec_Some [constructor, in MetaRocq.Utils.MRList]
nth_error_Spec [inductive, in MetaRocq.Utils.MRList]
nth_error_map [lemma, in MetaRocq.Utils.MRList]
nth_error_safe_nth [lemma, in MetaRocq.Utils.MRList]
nth_error_subst_context [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
nth_error_all_rels_spec [lemma, in MetaRocq.PCUIC.PCUICSpine]
nth_error_inds [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
nth_error_rename_context [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
nth_error_closed_context_lift [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_Some_add [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_closed_context [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_smash_context [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nth_error_ass_subst_context [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nth_error_map_InP [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nth_error_removelast [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
nth_map' [lemma, in MetaRocq.Template.EtaExpand]
nth_error_smash_onfvs [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
nth_error_expand_lets [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
nth_error_subst_instance [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
nth_error_size [lemma, in MetaRocq.PCUIC.utils.PCUICSize]
nth_map_option_out [lemma, in MetaRocq.Utils.MROption]
nth_error_idsn_eq_Some [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
nth_error_idsn_None [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
nth_error_idsn_Some [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
nth_ren_ids_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
nth_error_app_context_lt [lemma, in MetaRocq.Common.BasicAst]
nth_error_app_context_ge [lemma, in MetaRocq.Common.BasicAst]
nth_error_arities_context [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
nth_reorder_list_ctors [lemma, in MetaRocq.Erasure.EReorderCstrs]
nth_error_reorder [lemma, in MetaRocq.Erasure.EReorderCstrs]
nth_error_depth [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
nth_error_map_All [lemma, in MetaRocq.Utils.All_Forall]
nth_error_alli [lemma, in MetaRocq.Utils.All_Forall]
nth_error_all [lemma, in MetaRocq.Utils.All_Forall]
nth_error_forall [lemma, in MetaRocq.Utils.All_Forall]
nth_error_forallb [lemma, in MetaRocq.Utils.All_Forall]
nth_error_fold_context_k [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx_all_defs [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx_l [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
nth_error_map_In [lemma, in MetaRocq.ErasurePlugin.Erasure]
nth_error_closed_context [lemma, in MetaRocq.PCUIC.PCUICInversion]
nth_error_projs_inst [lemma, in MetaRocq.PCUIC.PCUICInductives]
nth_errror_arities_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
nth_error_rev_map [lemma, in MetaRocq.PCUIC.PCUICInductives]
nth_error_map2 [lemma, in MetaRocq.PCUIC.PCUICReduction]
nth_error_firstn_skipn [lemma, in MetaRocq.PCUIC.PCUICReduction]
nth_error_fix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
nth_error_cofix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
nth_error_map_fix [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
nth_error_assumption_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
nth_error_masked [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
nth_error_inst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
nth_error_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
nth_error_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
| 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) |