| 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 (definition)
nameless [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]nameless_decl [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
name_from_term [in MetaCoq.Erasure.EPretty]
name_from_term [in MetaCoq.Template.Pretty]
name_from_term [in MetaCoq.PCUIC.utils.PCUICPretty]
nAnon [in MetaCoq.Translations.translation_utils]
nAnon [in MetaCoq.Translations.param_binary]
nApp [in MetaCoq.PCUIC.utils.PCUICAstUtils]
Nbar.add [in MetaCoq.Template.utils.wGraph]
Nbar.add_max_distr_r [in MetaCoq.Template.utils.wGraph]
Nbar.add_0_r [in MetaCoq.Template.utils.wGraph]
Nbar.add_assoc [in MetaCoq.Template.utils.wGraph]
Nbar.le [in MetaCoq.Template.utils.wGraph]
Nbar.lt [in MetaCoq.Template.utils.wGraph]
Nbar.max [in MetaCoq.Template.utils.wGraph]
Nbar.max_idempotent [in MetaCoq.Template.utils.wGraph]
Nbar.max_le' [in MetaCoq.Template.utils.wGraph]
Nbar.max_lub [in MetaCoq.Template.utils.wGraph]
Nbar.plus_le_compat [in MetaCoq.Template.utils.wGraph]
Nbar.plus_le_compat_l [in MetaCoq.Template.utils.wGraph]
Nbar.S [in MetaCoq.Template.utils.wGraph]
Nbar.sub [in MetaCoq.Template.utils.wGraph]
Nbar.t [in MetaCoq.Template.utils.wGraph]
neg_forall [in MetaCoq.Template.common.uGraph]
new_cstr [in MetaCoq.Examples.add_constructor]
nl [in MetaCoq.Template.utils.MCString]
nl [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nlctx [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nlctx_binders [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlg [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nlict [in MetaCoq.PCUIC.PCUICAst]
nl_global_env [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_global_declarations [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_global_decl [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_mutual_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_one_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_projection_body [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_constructor_body [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_constant_body [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_branch [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_predicate [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nNamed [in MetaCoq.Translations.translation_utils]
nNamed [in MetaCoq.Translations.param_binary]
noccur_shift [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
noccur_between [in MetaCoq.Template.Ast]
noccur_between [in MetaCoq.PCUIC.PCUICAst]
nocc_between [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
nocc_betweenp [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
nodelta_flags [in MetaCoq.Template.Checker]
NonEmptySetFacts.add [in MetaCoq.Template.Universes]
NonEmptySetFacts.add_list [in MetaCoq.Template.Universes]
NonEmptySetFacts.map [in MetaCoq.Template.Universes]
NonEmptySetFacts.non_empty_union [in MetaCoq.Template.Universes]
NonEmptySetFacts.singleton [in MetaCoq.Template.Universes]
NonEmptySetFacts.to_nonempty_list [in MetaCoq.Template.Universes]
not [in MetaCoq.Examples.tauto]
NotFunext [in MetaCoq.Translations.times_bool_fun]
| 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) |