| 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 (constructor)
nAnon [in MetaRocq.Common.BasicAst]NativeCast [in MetaRocq.Common.BasicAst]
ne_nf [in MetaRocq.PCUIC.PCUICNormal]
ne_proj [in MetaRocq.PCUIC.PCUICNormal]
ne_case [in MetaRocq.PCUIC.PCUICNormal]
ne_fixapp [in MetaRocq.PCUIC.PCUICNormal]
ne_const [in MetaRocq.PCUIC.PCUICNormal]
ne_app [in MetaRocq.PCUIC.PCUICNormal]
ne_evar [in MetaRocq.PCUIC.PCUICNormal]
ne_var [in MetaRocq.PCUIC.PCUICNormal]
ne_rel [in MetaRocq.PCUIC.PCUICNormal]
ne_proj [in MetaRocq.Template.Normal]
ne_case [in MetaRocq.Template.Normal]
ne_app [in MetaRocq.Template.Normal]
ne_const [in MetaRocq.Template.Normal]
ne_evar [in MetaRocq.Template.Normal]
ne_var [in MetaRocq.Template.Normal]
ne_rel [in MetaRocq.Template.Normal]
nf_tProd [in MetaRocq.PCUIC.PCUICNormal]
nf_tind [in MetaRocq.PCUIC.PCUICNormal]
nf_cofix [in MetaRocq.PCUIC.PCUICNormal]
nf_construct [in MetaRocq.PCUIC.PCUICNormal]
nf_lam [in MetaRocq.PCUIC.PCUICNormal]
nf_cofix [in MetaRocq.Template.Normal]
nf_fix [in MetaRocq.Template.Normal]
nf_indapp [in MetaRocq.Template.Normal]
nf_cstrapp [in MetaRocq.Template.Normal]
nf_lam [in MetaRocq.Template.Normal]
nf_prod [in MetaRocq.Template.Normal]
nf_sort [in MetaRocq.Template.Normal]
nf_ne [in MetaRocq.Template.Normal]
nNamed [in MetaRocq.Common.BasicAst]
normalization [in MetaRocq.PCUIC.PCUICSN]
normalization_in_adjust_universes [in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
normalization_in [in MetaRocq.PCUIC.PCUICSN]
NotAnArity [in MetaRocq.SafeChecker.PCUICErrors]
NotAnInductive [in MetaRocq.SafeChecker.PCUICErrors]
NotAnInductive [in MetaRocq.Template.Checker]
NotAProduct [in MetaRocq.SafeChecker.PCUICErrors]
NotAProduct [in MetaRocq.Template.Checker]
NotASort [in MetaRocq.SafeChecker.PCUICErrors]
NotASort [in MetaRocq.Template.Checker]
NotConvertible [in MetaRocq.SafeChecker.PCUICErrors]
NotConvertible [in MetaRocq.Template.Checker]
NotCumulSmaller [in MetaRocq.SafeChecker.PCUICErrors]
NotEnoughFuel [in MetaRocq.Template.Checker]
NotFoundConstant [in MetaRocq.SafeChecker.PCUICErrors]
NotFoundConstants [in MetaRocq.SafeChecker.PCUICErrors]
notSolvable [in MetaRocq.Examples.tauto]
NotSupported [in MetaRocq.Template.Checker]
nth_error_app_spec_out [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_right [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_left [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_Spec_None [in MetaRocq.Utils.MRList]
nth_error_Spec_Some [in MetaRocq.Utils.MRList]
| 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) |