| 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) |
Z
zerocst [definition, in MetaRocq.Examples.metarocq_tour]Zeta1 [library]
zip [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zip [definition, in MetaRocq.Template.Checker]
zipc [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zipc_stack_cat [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zipc_inj [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zipc_appstack [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zipc_unfold_decompose_stack [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
zipc_decompose_stack_empty [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
zipp [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zippx [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
zipp_noStackApp [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
zipp_as_mkApps [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
zipp_appstack [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
zipp_stack_cat [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
zipp_stack_cat_decompose_stack [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
zipx [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Z_as_int [instance, in MetaRocq.Common.Reflect]
Z_of_pos_alt [lemma, in MetaRocq.Utils.MRArith]
Z_of_nat_inj_bool [lemma, in MetaRocq.Common.uGraph]
Z_of_nat_bool_to_nat [lemma, in MetaRocq.Common.uGraph]
Z_of_bool [definition, in MetaRocq.Common.uGraph]