| 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 (lemma)
gcs_elements_union [in MetaRocq.Common.uGraph]GCS_pair_spec [in MetaRocq.Common.uGraph]
gc_levels_declared_union_or [in MetaRocq.Common.uGraph]
gc_of_uctx_levels [in MetaRocq.Common.uGraph]
gc_of_uctx_union [in MetaRocq.Common.uGraph]
gc_of_constraints_union [in MetaRocq.Common.uGraph]
gc_of_constraintsP [in MetaRocq.Common.uGraph]
gc_of_constraints_declared [in MetaRocq.Common.uGraph]
gc_leq0_universe_n_sup [in MetaRocq.Common.uGraph]
gc_level_declared_make_graph [in MetaRocq.Common.uGraph]
gc_of_uctx_invariants [in MetaRocq.Common.uGraph]
gc_of_constraint_iff [in MetaRocq.Common.uGraph]
gc_of_constraints_of_uctx [in MetaRocq.Common.uGraph]
gc_of_uctx_of_constraints [in MetaRocq.Common.uGraph]
gc_eq_universe_iff [in MetaRocq.Common.uGraph]
gc_leq_universe_iff [in MetaRocq.Common.uGraph]
gc_leq_universe_n_iff [in MetaRocq.Common.uGraph]
gc_eq0_universe_iff [in MetaRocq.Common.uGraph]
gc_leq0_universe_iff [in MetaRocq.Common.uGraph]
gc_leq0_universe_n_iff [in MetaRocq.Common.uGraph]
gc_consistent_iff [in MetaRocq.Common.uGraph]
gc_of_constraints_spec [in MetaRocq.Common.uGraph]
gc_of_constraint_spec [in MetaRocq.Common.uGraph]
gc_satisfies_singleton [in MetaRocq.Common.uGraph]
gc_satisfies_pair [in MetaRocq.Common.uGraph]
gen_transform_env_wf [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_decl_wf [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_wellformed_decl_irrel [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_wellformed_irrel [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_extends [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_eq [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_extends' [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env_wf [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_decl_wf [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_wellformed_decl_irrel [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_wellformed_irrel [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env_eq [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env_extends' [in MetaRocq.Erasure.EGenericMapEnv]
gen_many_fresh_length [in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh_fresh [in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh_aux_spec [in MetaRocq.Erasure.EWcbvEvalNamed]
get_is_level_correct [in MetaRocq.Common.Universes]
get_unboxable_case_branch_spec [in MetaRocq.Erasure.EUnboxing]
get_wt_indices [in MetaRocq.SafeChecker.PCUICSafeChecker]
get_level_make [in MetaRocq.SafeChecker.PCUICSafeConversion]
GlobalContextMap.constructor_isprop_pars_decl_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.global_context_map_ind [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_pars_args_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_kind_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constant_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_env_spec [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.make_irrel [in MetaRocq.Erasure.EEnvMap]
GlobalEnvMap.lookup_projection_spec [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_constructor_spec [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_inductive_spec [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_minductive_spec [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_env_spec [in MetaRocq.Template.TemplateEnvMap]
GlobalMaps.check_constructors_smaller_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_respects_variance_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_respects_variance_impl_gen [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global_iff_lookup_globals_nil [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global_iff_lookup_global_None [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global_iff_not_In [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_respects_variance_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lookup_on_global_env [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.NoDup_on_global_decls [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_impl_config [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_impl_simple [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_impl_only_config [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl_impl_full [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_variance_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructors_impl_config_gen [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructor_impl_config_gen [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_ext_empty_ext [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.sorts_local_ctx_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.sorts_local_ctx_impl_gen [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.type_local_ctx_impl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.type_local_ctx_impl_gen [in MetaRocq.Common.EnvironmentTyping]
global_ext_constraints_nlg [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
global_ext_levels_nlg [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
global_variance_nl_sigma_mon [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
global_variance_empty [in MetaRocq.PCUIC.PCUICEquality]
global_variance_napp_mon [in MetaRocq.PCUIC.PCUICEquality]
global_variance_sigma_mon [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
global_deps_empty [in MetaRocq.Erasure.ErasureFunction]
global_deps_kn [in MetaRocq.Erasure.ErasureFunction]
global_deps_subset [in MetaRocq.Erasure.ErasureFunction]
global_deps_union [in MetaRocq.Erasure.ErasureFunction]
global_variance_napp_mon [in MetaRocq.Template.TermEquality]
global_levels_sub [in MetaRocq.PCUIC.PCUICWeakeningEnv]
global_levels_union_set [in MetaRocq.PCUIC.PCUICWeakeningEnv]
global_ext_constraints_app [in MetaRocq.PCUIC.PCUICWeakeningEnv]
global_uctx_invariants__declare_and_uniquify_and_combine_levels [in MetaRocq.Common.UniversesDec]
global_erased_with_deps_weaken_prefix [in MetaRocq.Erasure.ErasureFunctionProperties]
global_env_ind [in MetaRocq.Erasure.ErasureFunctionProperties]
global_erases_with_deps_weaken [in MetaRocq.Erasure.ErasureFunctionProperties]
global_erases_with_deps_cons [in MetaRocq.Erasure.ErasureFunctionProperties]
global_subset_cons_right [in MetaRocq.Erasure.EExtends]
global_subset_cons [in MetaRocq.Erasure.EExtends]
global_subset_In [in MetaRocq.Erasure.EExtends]
global_erased_with_deps_erases_deps_tConst [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
global_context_set_sub_ext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_gc_uctx_invariants_union_or [in MetaRocq.Common.uGraph]
global_uctx_invariants_union_or [in MetaRocq.Common.uGraph]
global_uctx_graph_invariants [in MetaRocq.Common.uGraph]
global_uctx_invariants_ext [in MetaRocq.SafeChecker.PCUICTypeChecker]
global_ext_constraints_trans [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
global_ext_levels_trans [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
global_constraints_trans [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
global_levels_trans [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
GoodConstraintSet_pair_In [in MetaRocq.Common.uGraph]
GoodConstraint.compare_spec [in MetaRocq.Common.uGraph]
GoodConstraint.compare_refl [in MetaRocq.Common.uGraph]
GoodConstraint.compare_eq [in MetaRocq.Common.uGraph]
GoodConstraint.compare_trans [in MetaRocq.Common.uGraph]
GoodConstraint.compare_sym [in MetaRocq.Common.uGraph]
GoodConstraint.lt_compat [in MetaRocq.Common.uGraph]
GoodConstraint.lt_strorder [in MetaRocq.Common.uGraph]
GoodConstraint.lt_not_eq [in MetaRocq.Common.uGraph]
GoodConstraint.lt_trans [in MetaRocq.Common.uGraph]
GoodConstraint.nat_compare_eq [in MetaRocq.Common.uGraph]
GoodConstraint.nat_compare_trans [in MetaRocq.Common.uGraph]
GoodConstraint.Z_compare_trans [in MetaRocq.Common.uGraph]
graph_of_wf_ext [in MetaRocq.SafeChecker.PCUICEqualityDec]
graph_of_wf [in MetaRocq.SafeChecker.PCUICEqualityDec]
| 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) |