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) |
V (definition)
valid [in MetaCoq.Examples.tauto]validpos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
valid_constraints [in MetaCoq.Template.Universes]
valid_constraints0 [in MetaCoq.Template.Universes]
valid_gc_constraints_ext [in MetaCoq.Template.common.uGraph]
valid_gc_constraints [in MetaCoq.Template.common.uGraph]
valid_gc_constraint [in MetaCoq.Template.common.uGraph]
valid_subgoal [in MetaCoq.Examples.tauto]
valuation_of_labelling [in MetaCoq.Template.common.uGraph]
var [in MetaCoq.Examples.tauto]
VariableLevel.compare [in MetaCoq.Template.common.uGraph]
VariableLevel.compare_spec [in MetaCoq.Template.common.uGraph]
VariableLevel.eq_dec [in MetaCoq.Template.common.uGraph]
VariableLevel.lt [in MetaCoq.Template.common.uGraph]
VariableLevel.lt_compat [in MetaCoq.Template.common.uGraph]
VariableLevel.lt_trans [in MetaCoq.Template.common.uGraph]
VariableLevel.t [in MetaCoq.Template.common.uGraph]
VariableLevel.to_level [in MetaCoq.Template.common.uGraph]
VariableLevel.to_noprop [in MetaCoq.Template.common.uGraph]
variable_of_level [in MetaCoq.Template.common.uGraph]
vass [in MetaCoq.Erasure.EAst]
vass_open_decl [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
vdef [in MetaCoq.Erasure.EAst]
view_prod_sortc [in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_indc [in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prodc [in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_sortc [in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_construct0_cofix [in MetaCoq.PCUIC.Syntax.PCUICViews]
view_construct_cofix [in MetaCoq.PCUIC.Syntax.PCUICViews]