| 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 | (18986 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 | (297 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 | (8135 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 | (1490 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |
V (constructor)
val [in MetaRocq.Common.Universes]value_app [in MetaRocq.Template.WcbvEval]
value_atom [in MetaRocq.Template.WcbvEval]
value_head_fix [in MetaRocq.Template.WcbvEval]
value_head_ind [in MetaRocq.Template.WcbvEval]
value_head_cofix [in MetaRocq.Template.WcbvEval]
value_head_cstr [in MetaRocq.Template.WcbvEval]
value_app_nonnil [in MetaRocq.Erasure.EWcbvEval]
value_constructor [in MetaRocq.Erasure.EWcbvEval]
value_atom [in MetaRocq.Erasure.EWcbvEval]
value_head_fix [in MetaRocq.Erasure.EWcbvEval]
value_head_cofix [in MetaRocq.Erasure.EWcbvEval]
value_head_cstr [in MetaRocq.Erasure.EWcbvEval]
value_app_nonnil [in MetaRocq.PCUIC.PCUICWcbvEval]
value_atomic [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_fix [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_cofix [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_ind [in MetaRocq.PCUIC.PCUICWcbvEval]
value_head_cstr [in MetaRocq.PCUIC.PCUICWcbvEval]
VariableLevel.level [in MetaRocq.Common.uGraph]
VariableLevel.lvar [in MetaRocq.Common.uGraph]
Variance [in MetaRocq.Common.Universes]
Variance.Covariant [in MetaRocq.Common.Universes]
Variance.Invariant [in MetaRocq.Common.Universes]
Variance.Irrelevant [in MetaRocq.Common.Universes]
VarRef [in MetaRocq.Common.Kernames]
vClos [in MetaRocq.Erasure.EWcbvEvalNamed]
vConstruct [in MetaRocq.Erasure.EWcbvEvalNamed]
view_prod_other [in MetaRocq.Erasure.Typed.Erasure]
view_prod_prod [in MetaRocq.Erasure.Typed.Erasure]
view_other [in MetaRocq.SafeChecker.PCUICSafeReduce]
view_construct [in MetaRocq.SafeChecker.PCUICSafeReduce]
view_prod_sort_other [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_sort [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_prod [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_other [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_ind_tInd [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_other [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_prod_prod [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_other [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_sort_sort [in MetaRocq.PCUIC.utils.PCUICAstUtils]
view_other [in MetaRocq.Erasure.EEtaExpanded]
view_construct [in MetaRocq.Erasure.EEtaExpanded]
vLazy [in MetaRocq.Erasure.EWcbvEvalNamed]
VmCast [in MetaRocq.Common.BasicAst]
vPrim [in MetaRocq.Erasure.EWcbvEvalNamed]
vRecClos [in MetaRocq.Erasure.EWcbvEvalNamed]
| 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 | (18986 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 | (297 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 | (8135 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 | (1490 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 | (343 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 | (524 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 | (720 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 | (401 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 | (331 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 | (4701 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 | (178 entries) |