| 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) |
L (definition)
labelling_of_valuation [in MetaRocq.Common.uGraph]lam_body_annot_cont [in MetaRocq.Erasure.Typed.Annotations]
laxest_checker_flags [in MetaRocq.Common.config]
lengths [in MetaRocq.PCUIC.Syntax.PCUICTactics]
lengths [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
length_rev_transparent [in MetaRocq.Erasure.Typed.TypeAnnotations]
length_app_transparent [in MetaRocq.Erasure.Typed.TypeAnnotations]
leqb_sort_n_ [in MetaRocq.Common.Universes]
leqb_term [in MetaRocq.SafeChecker.PCUICEqualityDec]
leqb_univ_expr_n_spec' [in MetaRocq.Common.uGraph]
leqb_sort [in MetaRocq.Common.uGraph]
leqb_universe_n_spec [in MetaRocq.Common.uGraph]
leqb_universe_n_spec0 [in MetaRocq.Common.uGraph]
leqb_universe_n [in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec [in MetaRocq.Common.uGraph]
leqb_expr_univ_n_spec0 [in MetaRocq.Common.uGraph]
leqb_expr_univ_n [in MetaRocq.Common.uGraph]
leqb_expr_n_spec [in MetaRocq.Common.uGraph]
leqb_expr_n_spec0 [in MetaRocq.Common.uGraph]
leqb_expr_n [in MetaRocq.Common.uGraph]
leqb_level_n_spec_gen [in MetaRocq.Common.uGraph]
leqb_level_n [in MetaRocq.Common.uGraph]
leqb_sort_gen [in MetaRocq.Common.uGraph]
leqb_universe_n_gen [in MetaRocq.Common.uGraph]
leqb_expr_univ_n_gen [in MetaRocq.Common.uGraph]
leqb_expr_n_gen [in MetaRocq.Common.uGraph]
leq_sort_refl' [in MetaRocq.Common.Universes]
leq_csort [in MetaRocq.Common.Universes]
leq_csort_n [in MetaRocq.Common.Universes]
leq_sort [in MetaRocq.Common.Universes]
leq_sort_n [in MetaRocq.Common.Universes]
leq_sort_n_ [in MetaRocq.Common.Universes]
leq_universe_refl' [in MetaRocq.Common.Universes]
leq_universe [in MetaRocq.Common.Universes]
leq_universe_n [in MetaRocq.Common.Universes]
leq_universe_n_dec [in MetaRocq.Common.UniversesDec]
leq_term_nocast [in MetaRocq.Template.Typing]
leq_term [in MetaRocq.Template.Checker]
leq0_universe_n [in MetaRocq.Common.Universes]
leq0_universe_n_dec [in MetaRocq.Common.UniversesDec]
leq0_level_n_complete [in MetaRocq.Common.uGraph]
leq0_level_n [in MetaRocq.Common.uGraph]
LevelExpr.compare [in MetaRocq.Common.Universes]
LevelExpr.compare_spec [in MetaRocq.Common.Universes]
LevelExpr.eq [in MetaRocq.Common.Universes]
LevelExpr.eq_leibniz [in MetaRocq.Common.Universes]
LevelExpr.eq_dec [in MetaRocq.Common.Universes]
LevelExpr.eq_equiv [in MetaRocq.Common.Universes]
LevelExpr.get_noprop [in MetaRocq.Common.Universes]
LevelExpr.get_level [in MetaRocq.Common.Universes]
LevelExpr.is_level [in MetaRocq.Common.Universes]
LevelExpr.lt [in MetaRocq.Common.Universes]
LevelExpr.lt_compat [in MetaRocq.Common.Universes]
LevelExpr.lt__sind [in MetaRocq.Common.Universes]
LevelExpr.lt__ind [in MetaRocq.Common.Universes]
LevelExpr.make [in MetaRocq.Common.Universes]
LevelExpr.set [in MetaRocq.Common.Universes]
LevelExpr.succ [in MetaRocq.Common.Universes]
LevelExpr.t [in MetaRocq.Common.Universes]
LevelExpr.type1 [in MetaRocq.Common.Universes]
LevelSetsUIP.eqb_LevelSet [in MetaRocq.Common.Reflect]
LevelSetsUIP.levels_tree_rect [in MetaRocq.Common.Reflect]
LevelSetsUIP.levels_tree_eqb [in MetaRocq.Common.Reflect]
LevelSet_mem_union [in MetaRocq.Common.Universes]
LevelSet_pair [in MetaRocq.Common.Universes]
levels_of_udecl [in MetaRocq.Common.Universes]
levels_of_universe [in MetaRocq.Common.UniversesDec]
levels_of_cscs [in MetaRocq.Common.UniversesDec]
levels_of_cs2 [in MetaRocq.Common.UniversesDec]
levels_of_cs [in MetaRocq.Common.UniversesDec]
level_lt_ind_dep [in MetaRocq.Common.Reflect]
level_mem [in MetaRocq.SafeChecker.PCUICWfEnv]
Level.compare [in MetaRocq.Common.Universes]
Level.compare_spec [in MetaRocq.Common.Universes]
Level.eq [in MetaRocq.Common.Universes]
Level.eqb [in MetaRocq.Common.Universes]
Level.eq_dec [in MetaRocq.Common.Universes]
Level.eq_leibniz [in MetaRocq.Common.Universes]
Level.eq_level [in MetaRocq.Common.Universes]
Level.eq_equiv [in MetaRocq.Common.Universes]
Level.is_var [in MetaRocq.Common.Universes]
Level.is_set [in MetaRocq.Common.Universes]
Level.lt [in MetaRocq.Common.Universes]
Level.lt_compat [in MetaRocq.Common.Universes]
Level.lt_strorder [in MetaRocq.Common.Universes]
Level.lt__sind [in MetaRocq.Common.Universes]
Level.lt__ind [in MetaRocq.Common.Universes]
Level.t [in MetaRocq.Common.Universes]
Level.t__sind [in MetaRocq.Common.Universes]
Level.t__rec [in MetaRocq.Common.Universes]
Level.t__ind [in MetaRocq.Common.Universes]
Level.t__rect [in MetaRocq.Common.Universes]
lexprod [in MetaRocq.PCUIC.utils.PCUICUtils]
le_ind_prop [in MetaRocq.Common.Reflect]
lift [in MetaRocq.PCUIC.PCUICAst]
lift [in MetaRocq.Template.Ast]
lift [in MetaRocq.Erasure.ELiftSubst]
lift_context_snoc0 [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
lift_namesM [in MetaRocq.Template.AstUtils]
lift_names [in MetaRocq.Template.AstUtils]
lift_ws [in MetaRocq.PCUIC.PCUICConfluence]
lift_ctx [in MetaRocq.Template.EtaExpand]
lift_wfext [in MetaRocq.ErasurePlugin.ErasureCorrectness]
lift_renaming [in MetaRocq.PCUIC.PCUICSigmaCalculus]
lift_mutual_inductive_body [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
lift_context_snoc0 [in MetaRocq.Template.TypingWf]
ListOrderedType.compare [in MetaRocq.Utils.MRCompare]
ListOrderedType.compare_spec [in MetaRocq.Utils.MRCompare]
ListOrderedType.eq [in MetaRocq.Utils.MRCompare]
ListOrderedType.eqb [in MetaRocq.Utils.MRCompare]
ListOrderedType.eqb_dec [in MetaRocq.Utils.MRCompare]
ListOrderedType.eq_leibniz [in MetaRocq.Utils.MRCompare]
ListOrderedType.eq_equiv [in MetaRocq.Utils.MRCompare]
ListOrderedType.lt [in MetaRocq.Utils.MRCompare]
ListOrderedType.lt__sind [in MetaRocq.Utils.MRCompare]
ListOrderedType.lt__ind [in MetaRocq.Utils.MRCompare]
ListOrderedType.t [in MetaRocq.Utils.MRCompare]
list_size [in MetaRocq.Utils.MRList]
list_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
list_context_sind [in MetaRocq.PCUIC.PCUICReduction]
list_context_rec [in MetaRocq.PCUIC.PCUICReduction]
list_context_ind [in MetaRocq.PCUIC.PCUICReduction]
list_context_rect [in MetaRocq.PCUIC.PCUICReduction]
local_entry_sind [in MetaRocq.PCUIC.PCUICAst]
local_entry_rec [in MetaRocq.PCUIC.PCUICAst]
local_entry_ind [in MetaRocq.PCUIC.PCUICAst]
local_entry_rect [in MetaRocq.PCUIC.PCUICAst]
local_entry_sind [in MetaRocq.Erasure.EAst]
local_entry_rec [in MetaRocq.Erasure.EAst]
local_entry_ind [in MetaRocq.Erasure.EAst]
local_entry_rect [in MetaRocq.Erasure.EAst]
lookup [in MetaRocq.Erasure.EWcbvEvalNamed]
lookup [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
lookup_ind_decl [in MetaRocq.Template.Pretty]
lookup_constructor_full [in MetaRocq.Erasure.Typed.ExAst]
lookup_constructor [in MetaRocq.Erasure.Typed.ExAst]
lookup_inductive [in MetaRocq.Erasure.Typed.ExAst]
lookup_minductive [in MetaRocq.Erasure.Typed.ExAst]
lookup_constant [in MetaRocq.Erasure.Typed.ExAst]
lookup_env [in MetaRocq.Erasure.Typed.ExAst]
lookup_inductive [in MetaRocq.Template.AstUtils]
lookup_minductive [in MetaRocq.Template.AstUtils]
lookup_mind_decl [in MetaRocq.Template.AstUtils]
lookup_constant [in MetaRocq.Erasure.ErasureProperties]
lookup_ind_decl [in MetaRocq.SafeChecker.PCUICSafeRetyping]
lookup_global_env [in MetaRocq.Template.EtaExpand]
lookup_ind_decl [in MetaRocq.PCUIC.utils.PCUICPretty]
lookup_constructor_ordinal [in MetaRocq.Erasure.EReorderCstrs]
lookup_constructor_mapping [in MetaRocq.Erasure.EReorderCstrs]
lookup_inductive_assoc [in MetaRocq.Erasure.EReorderCstrs]
lookup_env [in MetaRocq.Template.Checker]
lookup_constructor_type_cstrs [in MetaRocq.Template.Checker]
lookup_constructor_type [in MetaRocq.Template.Checker]
lookup_constructor_decl [in MetaRocq.Template.Checker]
lookup_ind_type_cstrs [in MetaRocq.Template.Checker]
lookup_ind_type [in MetaRocq.Template.Checker]
lookup_ind_decl [in MetaRocq.Template.Checker]
lookup_constant_type_cstrs [in MetaRocq.Template.Checker]
lookup_constant_type [in MetaRocq.Template.Checker]
lookup_ind_decl [in MetaRocq.Erasure.EPretty]
lookup_ind_decl [in MetaRocq.SafeChecker.PCUICTypeChecker]
lookup_projection [in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor_pars_args [in MetaRocq.Erasure.EGlobalEnv]
lookup_constructor [in MetaRocq.Erasure.EGlobalEnv]
lookup_inductive_kind [in MetaRocq.Erasure.EGlobalEnv]
lookup_inductive_pars [in MetaRocq.Erasure.EGlobalEnv]
lookup_inductive [in MetaRocq.Erasure.EGlobalEnv]
lookup_minductive [in MetaRocq.Erasure.EGlobalEnv]
lookup_constant [in MetaRocq.Erasure.EGlobalEnv]
lookup_env [in MetaRocq.Erasure.EGlobalEnv]
Lookup.consistent_instance_ext [in MetaRocq.Common.EnvironmentTyping]
Lookup.consistent_instance [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_projection [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_projection_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constructor [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constructor_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_inductive [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_inductive_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_minductive [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_minductive_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constant [in MetaRocq.Common.EnvironmentTyping]
Lookup.declared_constant_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_uctx [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_constraints [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_ext_levels [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_uctx [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_constraints [in MetaRocq.Common.EnvironmentTyping]
Lookup.global_levels [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_projection [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_projection_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constructor [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constructor_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_inductive [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_inductive_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_minductive [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_minductive_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constant [in MetaRocq.Common.EnvironmentTyping]
Lookup.lookup_constant_gen [in MetaRocq.Common.EnvironmentTyping]
Lookup.on_udecl_decl [in MetaRocq.Common.EnvironmentTyping]
Lookup.universes_decl_of_decl [in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_sort_dec [in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_universe_dec [in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_sort [in MetaRocq.Common.EnvironmentTyping]
Lookup.wf_universe [in MetaRocq.Common.EnvironmentTyping]
lsp_expr [in MetaRocq.Common.uGraph]
lt [in MetaRocq.Utils.ByteCompareSpec]
lt_csort [in MetaRocq.Common.Universes]
lt_sort [in MetaRocq.Common.Universes]
lt_universe [in MetaRocq.Common.Universes]
| 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) |