| 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 (definition)
gcs_equal [in MetaRocq.SafeChecker.PCUICSafeChecker]gcs_levels_declared [in MetaRocq.Common.uGraph]
gcs_equal [in MetaRocq.Common.uGraph]
gctx [in MetaRocq.Examples.typing_correctness]
gctx [in MetaRocq.Examples.metarocq_tour_prelude]
gctx_wf_env [in MetaRocq.Examples.typing_correctness]
gctx_wf_env [in MetaRocq.Examples.metarocq_tour_prelude]
gctx_union [in MetaRocq.Common.uGraph]
gc_result_eq [in MetaRocq.Common.uGraph]
gc_eq_sort [in MetaRocq.Common.uGraph]
gc_leq_sort [in MetaRocq.Common.uGraph]
gc_levels_declared' [in MetaRocq.Common.uGraph]
gc_levels_declared_sort [in MetaRocq.Common.uGraph]
gc_levels_declared [in MetaRocq.Common.uGraph]
gc_expr_declared [in MetaRocq.Common.uGraph]
gc_level_declared [in MetaRocq.Common.uGraph]
gc_of_uctx [in MetaRocq.Common.uGraph]
gc_lt_universe [in MetaRocq.Common.uGraph]
gc_leq_universe [in MetaRocq.Common.uGraph]
gc_lt0_universe [in MetaRocq.Common.uGraph]
gc_leq0_universe [in MetaRocq.Common.uGraph]
gc_eq_universe [in MetaRocq.Common.uGraph]
gc_eq0_universe [in MetaRocq.Common.uGraph]
gc_leq_universe_n [in MetaRocq.Common.uGraph]
gc_leq0_universe_n [in MetaRocq.Common.uGraph]
gc_of_constraints [in MetaRocq.Common.uGraph]
gc_of_constraint [in MetaRocq.Common.uGraph]
gc_consistent [in MetaRocq.Common.uGraph]
gc_satisfies [in MetaRocq.Common.uGraph]
generate_proof_term [in MetaRocq.Erasure.Typed.Certifying]
gen_transform_env' [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_decl [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_constant_decl [in MetaRocq.Erasure.EGenericGlobalMap]
gen_transform_env' [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_env [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_decl [in MetaRocq.Erasure.EGenericMapEnv]
gen_transform_constant_decl [in MetaRocq.Erasure.EGenericMapEnv]
gen_defs_and_proofs [in MetaRocq.Erasure.Typed.Certifying]
gen_proof [in MetaRocq.Erasure.Typed.Certifying]
gen_prog [in MetaRocq.Erasure.Typed.Certifying]
gen_many_fresh [in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh [in MetaRocq.Erasure.EWcbvEvalNamed]
gen_fresh_aux [in MetaRocq.Erasure.EWcbvEvalNamed]
get_projections [in MetaRocq.Erasure.Typed.Extraction]
get_last_type_var [in MetaRocq.Erasure.Typed.TypeAnnotations]
get_unboxable_case_branch [in MetaRocq.Erasure.EUnboxing]
get_inductive_tvars [in MetaRocq.Erasure.Typed.Optimize]
get_const_mask [in MetaRocq.Erasure.Typed.Optimize]
get_ctor_mask [in MetaRocq.Erasure.Typed.Optimize]
get_branch_mask [in MetaRocq.Erasure.Typed.Optimize]
get_mib_masks [in MetaRocq.Erasure.Typed.Optimize]
get_eta_info [in MetaRocq.Erasure.Typed.CertifyingEta]
get_ind_info [in MetaRocq.Erasure.Typed.CertifyingEta]
get_def_name [in MetaRocq.Erasure.Typed.Certifying]
get_kername [in MetaRocq.Template.Lib]
GlobalContextMap.add [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.constructor_isprop_pars_decl [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.empty [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.global_context_map_equal [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_pars_args [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_kind [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_constant [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.lookup_env [in MetaRocq.Erasure.EEnvMap]
GlobalContextMap.make [in MetaRocq.Erasure.EEnvMap]
GlobalEnvMap.lookup_projection [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_constructor [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_inductive [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_minductive [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.lookup_env [in MetaRocq.Template.TemplateEnvMap]
GlobalEnvMap.make [in MetaRocq.Template.TemplateEnvMap]
GlobalMaps.check_ind_sorts [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.check_constructors_smaller [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.constructor_univs [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_concl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_concl_head [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.cstr_respects_variance [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.elim_sort_sprop_ind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.elim_sort_prop_ind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.fresh_global [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_respects_variance [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_arities [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.ind_realargs [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.level_var_instance [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_constraints [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_constraint [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_instance [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.lift_level [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.mdecl_at_i [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env_ext [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_env [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_univs [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_sind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_rec [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_ind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decls_rect [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_global_decl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constant_decl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_variance [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_projection [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_constructors [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_udecl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_type [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.on_context [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_sind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_rec [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_ind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_rect [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_sind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_rec [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_ind [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_rect [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.satisfiable_udecl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.sorts_local_ctx [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.type_local_ctx [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.univs_ext_constraints [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.valid_on_mono_udecl [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.variance_universes [in MetaRocq.Common.EnvironmentTyping]
GlobalMaps.variance_cstrs [in MetaRocq.Common.EnvironmentTyping]
globals_erased_with_deps [in MetaRocq.Erasure.EDeps]
global_decl_annots [in MetaRocq.Erasure.Typed.Annotations]
global_variance_gen [in MetaRocq.PCUIC.PCUICEquality]
global_env_ext_map_global_env_map [in MetaRocq.PCUIC.PCUICProgram]
global_env_ext_map_global_env_ext [in MetaRocq.PCUIC.PCUICProgram]
global_env_ext_map [in MetaRocq.PCUIC.PCUICProgram]
global_deps [in MetaRocq.Erasure.ErasureFunction]
global_decl_deps [in MetaRocq.Erasure.ErasureFunction]
global_env [in MetaRocq.Erasure.Typed.ExAst]
global_decl_sind [in MetaRocq.Erasure.Typed.ExAst]
global_decl_rec [in MetaRocq.Erasure.Typed.ExAst]
global_decl_ind [in MetaRocq.Erasure.Typed.ExAst]
global_decl_rect [in MetaRocq.Erasure.Typed.ExAst]
global_variance_gen [in MetaRocq.Template.TermEquality]
global_declarations_size [in MetaRocq.PCUIC.PCUICTyping]
global_ext_uctx_consistent [in MetaRocq.PCUIC.PCUICGlobalEnv]
global_erased_with_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
global_env_ext_map_global_env_ext [in MetaRocq.Template.EtaExpand]
global_env_ext_map_global_env_map [in MetaRocq.Template.EtaExpand]
global_env_ext_map [in MetaRocq.Template.EtaExpand]
global_subset [in MetaRocq.Erasure.EExtends]
global_uctx_univs [in MetaRocq.SafeChecker.PCUICSafeChecker]
global_reference_sind [in MetaRocq.Common.Kernames]
global_reference_rec [in MetaRocq.Common.Kernames]
global_reference_ind [in MetaRocq.Common.Kernames]
global_reference_rect [in MetaRocq.Common.Kernames]
global_declarations [in MetaRocq.Erasure.EAst]
global_decl_sind [in MetaRocq.Erasure.EAst]
global_decl_rec [in MetaRocq.Erasure.EAst]
global_decl_ind [in MetaRocq.Erasure.EAst]
global_decl_rect [in MetaRocq.Erasure.EAst]
global_context_set [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_ext_context_set [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_gc_uctx_invariants [in MetaRocq.Common.uGraph]
global_uctx_invariants [in MetaRocq.Common.uGraph]
globdecls_size [in MetaRocq.Template.Typing]
globenv_size [in MetaRocq.PCUIC.PCUICTyping]
globenv_size [in MetaRocq.Template.Typing]
GoodConstraintSet_pair [in MetaRocq.Common.uGraph]
GoodConstraint.compare [in MetaRocq.Common.uGraph]
GoodConstraint.eq [in MetaRocq.Common.uGraph]
GoodConstraint.eq_dec [in MetaRocq.Common.uGraph]
GoodConstraint.eq_equiv [in MetaRocq.Common.uGraph]
GoodConstraint.eq_trans [in MetaRocq.Common.uGraph]
GoodConstraint.eq_sym [in MetaRocq.Common.uGraph]
GoodConstraint.eq_refl [in MetaRocq.Common.uGraph]
GoodConstraint.lt [in MetaRocq.Common.uGraph]
GoodConstraint.satisfies [in MetaRocq.Common.uGraph]
GoodConstraint.t [in MetaRocq.Common.uGraph]
GoodConstraint.t__sind [in MetaRocq.Common.uGraph]
GoodConstraint.t__rec [in MetaRocq.Common.uGraph]
GoodConstraint.t__ind [in MetaRocq.Common.uGraph]
GoodConstraint.t__rect [in MetaRocq.Common.uGraph]
gref_eq_dec [in MetaRocq.Common.Kernames]
gref_eqb [in MetaRocq.Common.Kernames]
ground_quotable_of_iff [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_iffT [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_neq_of_EqDec [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_neg_of_dec [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_dec [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_neg_of_bp [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_bp [in MetaRocq.Quotation.ToPCUIC.Init]
ground_quotable_of_iff [in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_of_iffT [in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_neq_of_EqDec [in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_neg_of_dec [in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_of_dec [in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_neg_of_bp [in MetaRocq.Quotation.ToTemplate.Init]
ground_quotable_of_bp [in MetaRocq.Quotation.ToTemplate.Init]
guarded_to_unguarded_fix [in MetaRocq.ErasurePlugin.ETransform]
| 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) |