| 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) |
G
GC [section, in MetaRocq.Common.uGraph]GcOfConstraint [section, in MetaRocq.Common.uGraph]
GCS [module, in MetaRocq.Common.uGraph]
gcs_equal [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
gcs_elements_union [lemma, in MetaRocq.Common.uGraph]
gcs_levels_declared [definition, in MetaRocq.Common.uGraph]
GCS_pair_spec [lemma, in MetaRocq.Common.uGraph]
GCS_For_all_Proper [instance, in MetaRocq.Common.uGraph]
gcs_equal [definition, in MetaRocq.Common.uGraph]
gctx [definition, in MetaRocq.Examples.typing_correctness]
gctx [definition, in MetaRocq.Examples.metarocq_tour_prelude]
gctx_wf_env [definition, in MetaRocq.Examples.typing_correctness]
gctx_wf_env [definition, in MetaRocq.Examples.metarocq_tour_prelude]
gctx_union [definition, in MetaRocq.Common.uGraph]
gc_of_constraints_proper [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
gc_levels_declared_union_or [lemma, in MetaRocq.Common.uGraph]
gc_of_uctx_levels [lemma, in MetaRocq.Common.uGraph]
gc_of_constraints_proper [instance, in MetaRocq.Common.uGraph]
gc_of_uctx_union [lemma, in MetaRocq.Common.uGraph]
gc_of_constraints_union [lemma, in MetaRocq.Common.uGraph]
gc_of_constraintsP [lemma, in MetaRocq.Common.uGraph]
gc_of_constraints_none [constructor, in MetaRocq.Common.uGraph]
gc_of_constraints_ok [constructor, in MetaRocq.Common.uGraph]
gc_of_constraints_view [inductive, in MetaRocq.Common.uGraph]
gc_result_eq [definition, in MetaRocq.Common.uGraph]
gc_of_constraints_declared [lemma, in MetaRocq.Common.uGraph]
gc_eq_sort [definition, in MetaRocq.Common.uGraph]
gc_leq_sort [definition, in MetaRocq.Common.uGraph]
gc_levels_declared' [definition, in MetaRocq.Common.uGraph]
gc_leq0_universe_n_sup [lemma, in MetaRocq.Common.uGraph]
gc_levels_declared_sort [definition, in MetaRocq.Common.uGraph]
gc_levels_declared [definition, in MetaRocq.Common.uGraph]
gc_expr_declared [definition, in MetaRocq.Common.uGraph]
gc_level_declared_make_graph [lemma, in MetaRocq.Common.uGraph]
gc_level_declared [definition, in MetaRocq.Common.uGraph]
gc_of_uctx_invariants [lemma, in MetaRocq.Common.uGraph]
gc_of_constraint_iff [lemma, in MetaRocq.Common.uGraph]
gc_of_constraints_of_uctx [lemma, in MetaRocq.Common.uGraph]
gc_of_uctx_of_constraints [lemma, in MetaRocq.Common.uGraph]
gc_of_uctx [definition, in MetaRocq.Common.uGraph]
gc_eq_universe_iff [lemma, in MetaRocq.Common.uGraph]
gc_leq_universe_iff [lemma, in MetaRocq.Common.uGraph]
gc_leq_universe_n_iff [lemma, in MetaRocq.Common.uGraph]
gc_eq0_universe_iff [lemma, in MetaRocq.Common.uGraph]
gc_leq0_universe_iff [lemma, in MetaRocq.Common.uGraph]
gc_leq0_universe_n_iff [lemma, in MetaRocq.Common.uGraph]
gc_lt_universe [definition, in MetaRocq.Common.uGraph]
gc_leq_universe [definition, in MetaRocq.Common.uGraph]
gc_lt0_universe [definition, in MetaRocq.Common.uGraph]
gc_leq0_universe [definition, in MetaRocq.Common.uGraph]
gc_eq_universe [definition, in MetaRocq.Common.uGraph]
gc_eq0_universe [definition, in MetaRocq.Common.uGraph]
gc_leq_universe_n [definition, in MetaRocq.Common.uGraph]
gc_leq0_universe_n [definition, in MetaRocq.Common.uGraph]
gc_consistent_iff [lemma, in MetaRocq.Common.uGraph]
gc_of_constraints_spec [lemma, in MetaRocq.Common.uGraph]
gc_of_constraints [definition, in MetaRocq.Common.uGraph]
gc_of_constraint_spec [lemma, in MetaRocq.Common.uGraph]
gc_satisfies_singleton [lemma, in MetaRocq.Common.uGraph]
gc_of_constraint [definition, in MetaRocq.Common.uGraph]
gc_satisfies_pair [lemma, in MetaRocq.Common.uGraph]
gc_consistent [definition, in MetaRocq.Common.uGraph]
gc_satisfies [definition, in MetaRocq.Common.uGraph]
gc_satisfies0 [abbreviation, in MetaRocq.Common.uGraph]
GC.cf [variable, in MetaRocq.Common.uGraph]
GeneralizeOverHoles [library]
generate_proof_term [definition, in MetaRocq.Erasure.Typed.Certifying]
Generation [section, in MetaRocq.PCUIC.PCUICGeneration]
Generation.cf [variable, in MetaRocq.PCUIC.PCUICGeneration]
GenTransform [record, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformEnv [section, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformEnv.GT [variable, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformExtends [record, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformExtends [inductive, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformId [record, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformId [inductive, in MetaRocq.Erasure.EGenericGlobalMap]
GenTransformWf [record, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_wf [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_decl_wf [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_wellformed_decl_irrel [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_wellformed_irrel [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_extends [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_eq [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_extends' [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_wellformed [projection, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_inductive_decl_wf [projection, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_pre [projection, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env' [definition, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env [definition, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_decl [definition, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_constant_decl [definition, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_inductive_decl_id [projection, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_inductive_decl_id [constructor, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_inductive_decl [projection, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform [projection, in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_wf [lemma, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_decl_wf [lemma, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_wellformed_decl_irrel [lemma, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_wellformed_irrel [lemma, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env_eq [lemma, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env_extends' [lemma, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env' [definition, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env [definition, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_decl [definition, in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_constant_decl [definition, in MetaRocq.Erasure.EGenericMapEnv]
gen_defs_and_proofs [definition, in MetaRocq.Erasure.Typed.Certifying]
gen_proof [definition, in MetaRocq.Erasure.Typed.Certifying]
gen_prog [definition, in MetaRocq.Erasure.Typed.Certifying]
gen_many_fresh_length [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
gen_many_fresh [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh_fresh [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh_aux_spec [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh_aux [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
get_projections [definition, in MetaRocq.Erasure.Typed.Extraction]
get_is_level_correct [lemma, in MetaRocq.Common.Universes]
get_last_type_var [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
get_unboxable_case_branch_spec [lemma, in MetaRocq.Erasure.EUnboxing]
get_unboxable_case_branch [definition, in MetaRocq.Erasure.EUnboxing]
get_inductive_tvars [definition, in MetaRocq.Erasure.Typed.Optimize]
get_const_mask [definition, in MetaRocq.Erasure.Typed.Optimize]
get_ctor_mask [definition, in MetaRocq.Erasure.Typed.Optimize]
get_branch_mask [definition, in MetaRocq.Erasure.Typed.Optimize]
get_mib_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
get_eta_info [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
get_ind_info [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
get_wt_indices [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
get_def_name [definition, in MetaRocq.Erasure.Typed.Certifying]
get_const_mask [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
get_mib_masks [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
get_ctor_mask [abbreviation, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
get_level_make [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
get_kername [definition, in MetaRocq.Template.Lib]
give [abbreviation, in MetaRocq.SafeChecker.PCUICSafeReduce]
givePr [abbreviation, in MetaRocq.SafeChecker.PCUICSafeReduce]
givePr' [abbreviation, in MetaRocq.SafeChecker.PCUICSafeReduce]
Global [constructor, in MetaRocq.Template.TemplateMonad.Common]
global [constructor, in MetaRocq.Template.TemplateMonad.Common]
GlobalContextMap [module, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.add [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.constructor_isprop_pars_decl_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.constructor_isprop_pars_decl [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.empty [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.gceq [instance, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.global_context_map_ind [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.global_context_map_equal [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.global_decls [projection, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_pars_args_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_pars_args [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_kind_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_kind [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constant_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constant [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_env_spec [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_env [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.make [definition, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.make_irrel [lemma, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.map [projection, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.repr [projection, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.t [record, in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.wf [projection, in MetaRocq.Erasure.EEnvMap]
GlobalEnvMap [module, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.env [projection, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_projection_spec [lemma, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_projection [definition, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_constructor_spec [lemma, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_constructor [definition, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_inductive_spec [lemma, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_inductive [definition, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_minductive_spec [lemma, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_minductive [definition, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_env_spec [lemma, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_env [definition, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.make [definition, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.map [projection, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.repr [projection, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.t [record, in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.wf [projection, in MetaRocq.Template.TemplateEnvMap]
GlobalMaps [module, in MetaRocq.Common.EnvironmentTyping]
GlobalMapsSig [module, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.check_constructors_smaller_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.check_ind_sorts [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.check_constructors_smaller [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.constructor_univs [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_respects_variance_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_respects_variance_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_eq [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_args_length [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_concl [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_concl_head [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_respects_variance [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.elim_sort_sprop_ind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.elim_sort_prop_ind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global_iff_lookup_globals_nil [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global_iff_lookup_global_None [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global_iff_not_In [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.GlobalMaps [section, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.GlobalMaps.cf [variable, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.GlobalMaps.P [variable, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.GlobalMaps.Pcmp [variable, in MetaRocq.Common.EnvironmentTyping]
_ @ _ ;;; _ |+> _ (type_scope) [notation, in MetaRocq.Common.EnvironmentTyping]
_ ;;; _ |arg+> _ (type_scope) [notation, in MetaRocq.Common.EnvironmentTyping]
_ { _ := _ } [notation, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.globenv_decl [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.globenv_nil [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_respects_variance_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_sorts [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_cunivs [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_arity_eq [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_respects_variance [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_arities [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_realargs [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.kn_fresh [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.level_var_instance [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_constraints [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_constraint [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_instance [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_level [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lookup_on_global_env [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.mdecl_at_i [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.NoDup_on_global_decls [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onArity [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onConstructors [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onIndices [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onInductives [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onNpars [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onParams [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onProjections [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.onVariance [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_impl_config [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_impl_simple [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_impl_only_config [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_impl_full [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_variance_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructors_impl_config_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructor_impl_config_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_ext_empty_ext [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_ext [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_univs [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_sind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_rec [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_ind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_rect [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls [inductive, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_d [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_udecl_udecl [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_data [record, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constant_decl [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_inductive [record, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_variance [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_ind_body [record, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projs [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projs_all [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projs_elim [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projs_noidx [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projs_record [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projections [record, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projection [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_proj_relevance [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_proj_type [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_proj_name [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_proj [record, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructors [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_lets_in_type [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_ctype_variance [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_ctype_positive [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_cindices [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_cargs [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_ctype [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructor [record, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_udecl [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_type [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_context [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_sind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_rec [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_ind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_rect [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr [inductive, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_sind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_rec [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_ind [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_rect [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg [inductive, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_ass [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_let [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_concl [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_arg_ass [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_arg_let [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_arg_concl [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.pos_arg_closed [constructor, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.satisfiable_udecl [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.sorts_local_ctx_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.sorts_local_ctx_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.sorts_local_ctx [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.subst0 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.type_local_ctx_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.type_local_ctx_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.type_local_ctx [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.udecl [projection, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.univs_ext_constraints [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.valid_on_mono_udecl [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.variance_universes [definition, in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.variance_cstrs [definition, in MetaRocq.Common.EnvironmentTyping]
globals_erased_with_deps [definition, in MetaRocq.Erasure.EDeps]
global_decl_annots [definition, in MetaRocq.Erasure.Typed.Annotations]
global_ext_constraints_nlg [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
global_ext_levels_nlg [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
global_variance_nl_sigma_mon [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
global_variance_empty [lemma, in MetaRocq.PCUIC.PCUICEquality]
global_variance_napp_mon [lemma, in MetaRocq.PCUIC.PCUICEquality]
global_variance [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
global_variance_gen [definition, in MetaRocq.PCUIC.PCUICEquality]
global_env_ext_map_global_env_map [definition, in MetaRocq.PCUIC.PCUICProgram]
global_env_ext_map_global_env_ext [definition, in MetaRocq.PCUIC.PCUICProgram]
global_env_ext_map [definition, in MetaRocq.PCUIC.PCUICProgram]
global_env_map [record, in MetaRocq.PCUIC.PCUICProgram]
global_variance_sigma_mon [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
global_deps_empty [lemma, in MetaRocq.Erasure.ErasureFunction]
global_deps_proper_subset [instance, in MetaRocq.Erasure.ErasureFunction]
global_deps_proper [instance, in MetaRocq.Erasure.ErasureFunction]
global_deps_kn [lemma, in MetaRocq.Erasure.ErasureFunction]
global_deps_subset [lemma, in MetaRocq.Erasure.ErasureFunction]
global_deps_union [lemma, in MetaRocq.Erasure.ErasureFunction]
global_deps [definition, in MetaRocq.Erasure.ErasureFunction]
global_decl_deps [definition, in MetaRocq.Erasure.ErasureFunction]
global_env [definition, in MetaRocq.Erasure.Typed.ExAst]
global_decl_sind [definition, in MetaRocq.Erasure.Typed.ExAst]
global_decl_rec [definition, in MetaRocq.Erasure.Typed.ExAst]
global_decl_ind [definition, in MetaRocq.Erasure.Typed.ExAst]
global_decl_rect [definition, in MetaRocq.Erasure.Typed.ExAst]
global_decl [inductive, in MetaRocq.Erasure.Typed.ExAst]
global_variance_napp_mon [lemma, in MetaRocq.Template.TermEquality]
global_variance [abbreviation, in MetaRocq.Template.TermEquality]
global_variance_gen [definition, in MetaRocq.Template.TermEquality]
global_levels_sub [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
global_levels_union_set [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
global_ext_constraints_app [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
global_declarations_size [definition, in MetaRocq.PCUIC.PCUICTyping]
global_uctx_invariants__declare_and_uniquify_and_combine_levels [lemma, in MetaRocq.Common.UniversesDec]
global_ext_uctx_consistent [definition, in MetaRocq.PCUIC.PCUICGlobalEnv]
global_erased_with_deps_weaken_prefix [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
global_env_ind [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
global_erases_with_deps_weaken [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
global_erases_with_deps_cons [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
global_erased_with_deps [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
global_env_ext_map_global_env_ext [definition, in MetaRocq.Template.EtaExpand]
global_env_ext_map_global_env_map [definition, in MetaRocq.Template.EtaExpand]
global_env_ext_map [definition, in MetaRocq.Template.EtaExpand]
global_subset_cons_right [lemma, in MetaRocq.Erasure.EExtends]
global_subset_cons [lemma, in MetaRocq.Erasure.EExtends]
global_subset_In [lemma, in MetaRocq.Erasure.EExtends]
global_subset [definition, in MetaRocq.Erasure.EExtends]
global_erased_with_deps_erases_deps_tConst [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
global_uctx_univs [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
global_reference_sind [definition, in MetaRocq.Common.Kernames]
global_reference_rec [definition, in MetaRocq.Common.Kernames]
global_reference_ind [definition, in MetaRocq.Common.Kernames]
global_reference_rect [definition, in MetaRocq.Common.Kernames]
global_reference [inductive, in MetaRocq.Common.Kernames]
global_context [abbreviation, in MetaRocq.Erasure.EAst]
global_declarations [definition, in MetaRocq.Erasure.EAst]
global_decl_sind [definition, in MetaRocq.Erasure.EAst]
global_decl_rec [definition, in MetaRocq.Erasure.EAst]
global_decl_ind [definition, in MetaRocq.Erasure.EAst]
global_decl_rect [definition, in MetaRocq.Erasure.EAst]
global_decl [inductive, in MetaRocq.Erasure.EAst]
global_context_set_sub_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_context_set [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_ext_context_set [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_gc_uctx_invariants_union_or [lemma, in MetaRocq.Common.uGraph]
global_uctx_invariants_union_or [lemma, in MetaRocq.Common.uGraph]
global_uctx_graph_invariants [lemma, in MetaRocq.Common.uGraph]
global_gc_uctx_invariants [definition, in MetaRocq.Common.uGraph]
global_uctx_invariants [definition, in MetaRocq.Common.uGraph]
global_uctx_invariants_ext [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
global_ext_constraints_trans [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
global_ext_levels_trans [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
global_constraints_trans [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
global_levels_trans [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
globdecls_size [definition, in MetaRocq.Template.Typing]
globenv_size [definition, in MetaRocq.PCUIC.PCUICTyping]
globenv_size [definition, in MetaRocq.Template.Typing]
GoodConstraint [module, in MetaRocq.Common.uGraph]
GoodConstraintSet [module, in MetaRocq.Common.uGraph]
GoodConstraintSetDecide [module, in MetaRocq.Common.uGraph]
GoodConstraintSetFact [module, in MetaRocq.Common.uGraph]
GoodConstraintSetProp [module, in MetaRocq.Common.uGraph]
GoodConstraintSet_pair_In [lemma, in MetaRocq.Common.uGraph]
GoodConstraintSet_pair [definition, in MetaRocq.Common.uGraph]
GoodConstraint.compare [definition, in MetaRocq.Common.uGraph]
GoodConstraint.compare_spec [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.compare_refl [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.compare_eq [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.compare_trans [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.compare_sym [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.eq [definition, in MetaRocq.Common.uGraph]
GoodConstraint.eq_dec [definition, in MetaRocq.Common.uGraph]
GoodConstraint.eq_equiv [definition, in MetaRocq.Common.uGraph]
GoodConstraint.eq_trans [definition, in MetaRocq.Common.uGraph]
GoodConstraint.eq_sym [definition, in MetaRocq.Common.uGraph]
GoodConstraint.eq_refl [definition, in MetaRocq.Common.uGraph]
GoodConstraint.gc_le_var_set [constructor, in MetaRocq.Common.uGraph]
GoodConstraint.gc_le_level_set [constructor, in MetaRocq.Common.uGraph]
GoodConstraint.gc_le_set_var [constructor, in MetaRocq.Common.uGraph]
GoodConstraint.gc_lt_set_level [constructor, in MetaRocq.Common.uGraph]
GoodConstraint.gc_le [constructor, in MetaRocq.Common.uGraph]
GoodConstraint.lt [definition, in MetaRocq.Common.uGraph]
GoodConstraint.lt_compat [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.lt_strorder [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.lt_not_eq [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.lt_trans [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.nat_compare_eq [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.nat_compare_trans [lemma, in MetaRocq.Common.uGraph]
GoodConstraint.satisfies [definition, in MetaRocq.Common.uGraph]
GoodConstraint.t [definition, in MetaRocq.Common.uGraph]
GoodConstraint.t__sind [definition, in MetaRocq.Common.uGraph]
GoodConstraint.t__rec [definition, in MetaRocq.Common.uGraph]
GoodConstraint.t__ind [definition, in MetaRocq.Common.uGraph]
GoodConstraint.t__rect [definition, in MetaRocq.Common.uGraph]
GoodConstraint.t_ [inductive, in MetaRocq.Common.uGraph]
GoodConstraint.Z_compare_trans [lemma, in MetaRocq.Common.uGraph]
_ ?= _ [notation, in MetaRocq.Common.uGraph]
GraphSpec [section, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.cf [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.G [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.guard [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.HG [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.HΣ [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.Hφ [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
GraphSpec.Σ [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
graph_of_wf_ext [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
graph_of_wf [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
gref_eq_dec [definition, in MetaRocq.Common.Kernames]
gref_eqb [definition, in MetaRocq.Common.Kernames]
grep_reflect_eq [instance, in MetaRocq.Common.Kernames]
ground_quotable_of_iff [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_iffT [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_neq_of_EqDec [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_neg_of_dec [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_dec [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_neg_of_bp [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_bp [definition, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable [record, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable [inductive, in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_iff [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_of_iffT [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_neq_of_EqDec [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_neg_of_dec [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_of_dec [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_neg_of_bp [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_of_bp [definition, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable [record, in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable [inductive, in MetaRocq.Quotation.ToTemplate.Init]
GT [instance, in MetaRocq.Erasure.EOptimizePropDiscr]
GT [instance, in MetaRocq.Erasure.EConstructorsAsBlocks]
GT [instance, in MetaRocq.Erasure.EInlineProjections]
GT [instance, in MetaRocq.Erasure.ERemoveParams]
GTExt [instance, in MetaRocq.Erasure.EOptimizePropDiscr]
GTExt [instance, in MetaRocq.Erasure.EConstructorsAsBlocks]
GTExt [instance, in MetaRocq.Erasure.EInlineProjections]
GTExt [instance, in MetaRocq.Erasure.ERemoveParams]
GTID [instance, in MetaRocq.Erasure.EOptimizePropDiscr]
GTID [instance, in MetaRocq.Erasure.EConstructorsAsBlocks]
GTID [instance, in MetaRocq.Erasure.EInlineProjections]
GTWf [instance, in MetaRocq.Erasure.EOptimizePropDiscr]
GTWf [instance, in MetaRocq.Erasure.EConstructorsAsBlocks]
GTWf [instance, in MetaRocq.Erasure.EInlineProjections]
GTWf [instance, in MetaRocq.Erasure.ERemoveParams]
gtwf_axioms_efl [projection, in MetaRocq.Erasure.EGenericGlobalMap]
guard [projection, in MetaRocq.PCUIC.PCUICTyping]
GuardChecker [record, in MetaRocq.PCUIC.PCUICTyping]
GuardChecker [record, in MetaRocq.Template.Typing]
GuardCheckerCorrect [record, in MetaRocq.PCUIC.PCUICGuardCondition]
guarded_to_unguarded_fix_pres_app [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
guarded_to_unguarded_fix_pres [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
guarded_to_unguarded_fix_extends' [instance, in MetaRocq.ErasurePlugin.ETransform]
guarded_to_unguarded_fix_extends [instance, in MetaRocq.ErasurePlugin.ETransform]
guarded_to_unguarded_fix [definition, in MetaRocq.ErasurePlugin.ETransform]
guard_checking_correct [axiom, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_rename [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_inst [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_subst_instance [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_context_cumulativity [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_extends [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_eq_term [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_red1 [projection, in MetaRocq.PCUIC.PCUICGuardCondition]
guard_checking [axiom, in MetaRocq.PCUIC.PCUICTyping]
guard_checking [axiom, in MetaRocq.Template.Typing]
guard_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
guard_impl [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
| 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) |