| 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) |
M (instance)
make_graph_proper [in MetaCoq.Template.common.uGraph]make_graph_invariants [in MetaCoq.Template.common.uGraph]
make_graph_proper [in MetaCoq.SafeChecker.PCUICSafeChecker]
mapi_context_proper [in MetaCoq.Template.BasicAst]
map_context_proper [in MetaCoq.Template.BasicAst]
map_decl_pointwise [in MetaCoq.Template.BasicAst]
map_decl_proper [in MetaCoq.Template.BasicAst]
map_branch_proper [in MetaCoq.Template.Ast]
map_predicate_proper' [in MetaCoq.Template.Ast]
map_predicate_proper [in MetaCoq.Template.Ast]
map_branch_proper [in MetaCoq.PCUIC.PCUICAst]
map_predicate_proper' [in MetaCoq.PCUIC.PCUICAst]
map_predicate_proper [in MetaCoq.PCUIC.PCUICAst]
map_def_ext [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
map2_Proper [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_Proper [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
modpath_EqDec [in MetaCoq.Template.Kernames]
monad_exc [in MetaCoq.Translations.translation_utils]
monad_exc [in MetaCoq.SafeChecker.PCUICErrors]
Monad_EnvCheck_wf_env_ext [in MetaCoq.SafeChecker.SafeTemplateChecker]
monad_exc [in MetaCoq.Template.Checker]
Monad_EnvCheck_X_env_ext_type [in MetaCoq.SafeChecker.PCUICSafeChecker]