| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |
N (lemma)
nameless_eq_term_spec [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]nameless_eqctx_IH [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nApp_mkApps [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nApp_isApp_false [in MetaCoq.PCUIC.PCUICWcbvEval]
nApp_decompose_app [in MetaCoq.Erasure.EAstUtils]
nApp_mkApps [in MetaCoq.Template.AstUtils]
nat_rev_ind [in MetaCoq.Template.utils.MCArith]
nat_recursion_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
nat_le_irrel [in MetaCoq.Template.Reflect]
Nbar_max_le [in MetaCoq.Template.common.uGraph]
Nbar_max_spec'' [in MetaCoq.Template.common.uGraph]
Nbar_max_spec' [in MetaCoq.Template.common.uGraph]
Nbar_max_spec [in MetaCoq.Template.common.uGraph]
Nbar.add_0_l [in MetaCoq.Template.utils.wGraph]
Nbar.add_finite [in MetaCoq.Template.utils.wGraph]
Nbar.eq_max [in MetaCoq.Template.utils.wGraph]
Nbar.fold_max_le' [in MetaCoq.Template.utils.wGraph]
Nbar.fold_max_le [in MetaCoq.Template.utils.wGraph]
Nbar.fold_max_In [in MetaCoq.Template.utils.wGraph]
Nbar.le_antisymm [in MetaCoq.Template.utils.wGraph]
Nbar.le_plus_r [in MetaCoq.Template.utils.wGraph]
Nbar.le_lt_dec [in MetaCoq.Template.utils.wGraph]
Nbar.le_dec [in MetaCoq.Template.utils.wGraph]
Nbar.max_None [in MetaCoq.Template.utils.wGraph]
Nbar.sub_diag [in MetaCoq.Template.utils.wGraph]
negb_is_true [in MetaCoq.PCUIC.PCUICNormal]
negb_False [in MetaCoq.PCUIC.PCUICCanonicity]
neqb [in MetaCoq.Template.utils.ReflectEq]
neval_to_stuck_fix_app [in MetaCoq.Erasure.EEtaExpandedFix]
neval_to_stuck_fix [in MetaCoq.Erasure.EEtaExpandedFix]
nil_prefix [in MetaCoq.Template.utils.MCList]
nisApp_mkApps [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nisArityHead_mkApps [in MetaCoq.PCUIC.PCUICWcbvEval]
nisBox_mkApps [in MetaCoq.Erasure.EAstUtils]
nisErasable_Propositional [in MetaCoq.Erasure.EArities]
nisFixApp_nisFix [in MetaCoq.Erasure.EEtaExpandedFix]
nisFix_mkApps [in MetaCoq.Erasure.EAstUtils]
nisLambda_mkApps [in MetaCoq.PCUIC.PCUICWcbvEval]
nisLambda_mkApps [in MetaCoq.Erasure.EAstUtils]
nIs_conv_to_Arity_isWfArity_elim [in MetaCoq.Erasure.EArities]
nIs_conv_to_Arity_nArity [in MetaCoq.Erasure.EArities]
nlctx_smash_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_length [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_lift_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_subst_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_fix_context_alt [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_app_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_spec [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlg_wf_local [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_two [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_is_allowed_elimination [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_global_ext_levels [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_global_levels [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul_ctx [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv_ctx [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul_decls [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv_decls [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_red1 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_branches [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_branch [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_predicate [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_forget_types [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_branch_type [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_branch_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cstr_branch_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_predicate_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_inst_case_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_inds [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets_ctx [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_lift_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_telescope [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets_k [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_extended_subst [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_to_extended_list [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_declared_constructor [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_declared_inductive [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_fix_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_pred_set_pparams [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_pred_set_preturn [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_decompose_app [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_context [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_decl' [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_decl [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_lift [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_mkApps [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_decompose_prod_assum [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_compare_term [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_term [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_leq_term [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_term_upto_univ [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_context_assumptions [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_destArity [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_lookup_env [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_spec [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_cofixpoint [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_check_one_cofix [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_wf_fixpoint [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_check_one_fix [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
NonEmptySetFacts.add_list_spec [in MetaCoq.Template.Universes]
NonEmptySetFacts.add_spec [in MetaCoq.Template.Universes]
NonEmptySetFacts.elements_not_empty [in MetaCoq.Template.Universes]
NonEmptySetFacts.eq_univ'' [in MetaCoq.Template.Universes]
NonEmptySetFacts.eq_univ' [in MetaCoq.Template.Universes]
NonEmptySetFacts.eq_univ [in MetaCoq.Template.Universes]
NonEmptySetFacts.In_to_nonempty_list_rev [in MetaCoq.Template.Universes]
NonEmptySetFacts.In_to_nonempty_list [in MetaCoq.Template.Universes]
NonEmptySetFacts.LevelExprSet_For_all_exprs [in MetaCoq.Template.Universes]
NonEmptySetFacts.LevelExprSet_for_all_false [in MetaCoq.Template.Universes]
NonEmptySetFacts.map_spec [in MetaCoq.Template.Universes]
NonEmptySetFacts.not_Empty_is_empty [in MetaCoq.Template.Universes]
NonEmptySetFacts.singleton_to_nonempty_list [in MetaCoq.Template.Universes]
NonEmptySetFacts.to_nonempty_list_spec' [in MetaCoq.Template.Universes]
NonEmptySetFacts.to_nonempty_list_spec [in MetaCoq.Template.Universes]
NonEmptySetFacts.univ_expr_eqb_comm [in MetaCoq.Template.Universes]
NonEmptySetFacts.univ_expr_eqb_true_iff [in MetaCoq.Template.Universes]
normalisation_upto [in MetaCoq.PCUIC.PCUICSN]
not_empty_map [in MetaCoq.Template.utils.MCList]
not_var_global_ext_levels [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
not_var_global_levels [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
nth_map' [in MetaCoq.Template.EtaExpand]
nth_error_smash_context [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_ass_subst_context [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_map_InP [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_removelast [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_map_All [in MetaCoq.Template.utils.All_Forall]
nth_error_alli [in MetaCoq.Template.utils.All_Forall]
nth_error_all [in MetaCoq.Template.utils.All_Forall]
nth_error_forall [in MetaCoq.Template.utils.All_Forall]
nth_error_forallb [in MetaCoq.Template.utils.All_Forall]
nth_nth_error' [in MetaCoq.Template.utils.MCList]
nth_nth_error [in MetaCoq.Template.utils.MCList]
nth_error_unfold_inv [in MetaCoq.Template.utils.MCList]
nth_error_unfold [in MetaCoq.Template.utils.MCList]
nth_error_snoc [in MetaCoq.Template.utils.MCList]
nth_error_rev_inv [in MetaCoq.Template.utils.MCList]
nth_error_rev [in MetaCoq.Template.utils.MCList]
nth_error_app_inv [in MetaCoq.Template.utils.MCList]
nth_error_app_lt [in MetaCoq.Template.utils.MCList]
nth_error_app_ge [in MetaCoq.Template.utils.MCList]
nth_error_skipn [in MetaCoq.Template.utils.MCList]
nth_error_removelast [in MetaCoq.Template.utils.MCList]
nth_error_skipn_add [in MetaCoq.Template.utils.MCList]
nth_map' [in MetaCoq.Template.utils.MCList]
nth_error_nil [in MetaCoq.Template.utils.MCList]
nth_error_app_left [in MetaCoq.Template.utils.MCList]
nth_error_spec [in MetaCoq.Template.utils.MCList]
nth_error_Some' [in MetaCoq.Template.utils.MCList]
nth_error_Some_non_nil [in MetaCoq.Template.utils.MCList]
nth_error_Some_length [in MetaCoq.Template.utils.MCList]
nth_error_mapi [in MetaCoq.Template.utils.MCList]
nth_error_mapi_rec [in MetaCoq.Template.utils.MCList]
nth_error_map [in MetaCoq.Template.utils.MCList]
nth_error_safe_nth [in MetaCoq.Template.utils.MCList]
nth_error_map2 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
nth_error_All_local_env_over [in MetaCoq.Template.Typing]
nth_error_All_local_env [in MetaCoq.Template.Typing]
nth_error_subst_context [in MetaCoq.PCUIC.PCUICSubstitution]
nth_error_on_free_vars_ctx [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
nth_error_projs_inst [in MetaCoq.PCUIC.PCUICInductives]
nth_errror_arities_context [in MetaCoq.PCUIC.PCUICInductives]
nth_error_rev_map [in MetaCoq.PCUIC.PCUICInductives]
nth_error_All_local_env [in MetaCoq.PCUIC.PCUICValidity]
nth_error_expand_lets [in MetaCoq.PCUIC.PCUICInductiveInversion]
nth_error_subst_instance [in MetaCoq.PCUIC.PCUICInductiveInversion]
nth_error_fold_context_k [in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx_all_defs [in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx_l [in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx [in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_idsn_eq_Some [in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_error_idsn_None [in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_error_idsn_Some [in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_ren_ids_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_error_closed_context [in MetaCoq.PCUIC.PCUICInversion]
nth_error_weak_context [in MetaCoq.PCUIC.PCUICAlpha]
nth_error_inds [in MetaCoq.PCUIC.PCUICFirstorder]
nth_error_smash_onfvs [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nth_error_closed_context_lift [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_Some_add [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_closed_context [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_inst_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
nth_error_list_size [in MetaCoq.Examples.tauto]
nth_map_option_out [in MetaCoq.Template.utils.MCOption]
nth_error_All_local_env_over [in MetaCoq.PCUIC.PCUICTyping]
nth_error_All_local_env [in MetaCoq.PCUIC.PCUICTyping]
nth_error_size [in MetaCoq.PCUIC.utils.PCUICSize]
nth_error_All_local_env [in MetaCoq.PCUIC.PCUICContextConversion]
nth_error_app_context [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_appP [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_lift_context_eq [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_lift_context [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_rename_context [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
nth_error_depth [in MetaCoq.PCUIC.Syntax.PCUICDepth]
nth_error_fix_subst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_cofix_subst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_map_fix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_assumption_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_arities_context [in MetaCoq.SafeChecker.PCUICSafeChecker]
nth_error_map2 [in MetaCoq.PCUIC.PCUICReduction]
nth_error_firstn_skipn [in MetaCoq.PCUIC.PCUICReduction]
nth_error_all_rels_spec [in MetaCoq.PCUIC.PCUICSpine]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |