| 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) |
I (definition)
iBox [in MetaRocq.Erasure.EImplementBox]idecl_binder [in MetaRocq.PCUIC.Syntax.PCUICCases]
ident [in MetaRocq.Common.Kernames]
ident_of_name [in MetaRocq.Erasure.EWcbvEvalNamed]
ids [in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
id_nat [in MetaRocq.Examples.demo]
iffT_l [in MetaRocq.Utils.MRRelations]
impl [in MetaRocq.Common.config]
implement_box_program [in MetaRocq.Erasure.EImplementBox]
implement_box_env [in MetaRocq.Erasure.EImplementBox]
implement_box_decl [in MetaRocq.Erasure.EImplementBox]
implement_box_constant_decl [in MetaRocq.Erasure.EImplementBox]
implement_box [in MetaRocq.Erasure.EImplementBox]
impl_ctrans [in MetaRocq.Common.config]
impl_trans [in MetaRocq.Common.config]
impl_crefl [in MetaRocq.Common.config]
impl_refl [in MetaRocq.Common.config]
impl_reflb [in MetaRocq.Common.config]
includes_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
include_supermodule_of_submodule_inclusion [in MetaRocq.Quotation.ToPCUIC.Init]
include_submodule_of_submodule_inclusion [in MetaRocq.Quotation.ToPCUIC.Init]
include_supermodule_of_submodule_inclusion [in MetaRocq.Quotation.ToTemplate.Init]
include_submodule_of_submodule_inclusion [in MetaRocq.Quotation.ToTemplate.Init]
inddecl_name [in MetaRocq.PCUIC.PCUICCasesHelper]
indpred_ctx [in MetaRocq.PCUIC.PCUICCasesHelper]
inds [in MetaRocq.PCUIC.PCUICAst]
inds [in MetaRocq.Template.Ast]
inductives_mapping [in MetaRocq.Erasure.EProgram]
inductive_mapping [in MetaRocq.Erasure.EProgram]
inductive_arity [in MetaRocq.Erasure.Extract]
inductive_isprop_and_pars [in MetaRocq.Erasure.EGlobalEnv]
ind_aname [in MetaRocq.Erasure.Typed.Erasure]
ind_binder [in MetaRocq.PCUIC.PCUICCasesContexts]
ind_predicate_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
ind_subst [in MetaRocq.PCUIC.Syntax.PCUICCases]
ind_predicate_context [in MetaRocq.Template.Ast]
infer [in MetaRocq.SafeChecker.PCUICSafeRetyping]
infer [in MetaRocq.Template.Checker]
infer [in MetaRocq.SafeChecker.PCUICTypeChecker]
infering_indu_size_pos [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_size_pos [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_size_pos [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_size_pos [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_size [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_size [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_size [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_size [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_sind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_rec [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_ind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_indu_rect [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_sind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_rec [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_ind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_prod_rect [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_sind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_rec [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_ind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sort_rect [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_sind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_rec [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_ind [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infering_rect [in MetaRocq.PCUIC.Bidirectional.BDTyping]
infer_and_print_template_program_with_guard [in MetaRocq.SafeCheckerPlugin.Extraction]
infer_as_prod [in MetaRocq.SafeChecker.PCUICSafeRetyping]
infer_as_sort [in MetaRocq.SafeChecker.PCUICSafeRetyping]
infer_replacement_inductive [in MetaRocq.Quotation.ToPCUIC.Init]
infer_and_print_template_program [in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
infer_template_program [in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
infer_sorts_local_ctx [in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_type_wf_env [in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_wf_env [in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_typing [in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_term [in MetaRocq.SafeChecker.PCUICSafeChecker]
infer_replacement_inductive [in MetaRocq.Quotation.ToTemplate.Init]
infer_term [in MetaRocq.Template.Checker]
infer_cumul [in MetaRocq.Template.Checker]
infer_type [in MetaRocq.Template.Checker]
infer_spine [in MetaRocq.Template.Checker]
infer_isType [in MetaRocq.SafeChecker.PCUICTypeChecker]
infer_type [in MetaRocq.SafeChecker.PCUICTypeChecker]
infer' [in MetaRocq.Template.Checker]
inh [in MetaRocq.Examples.typing_correctness]
inh [in MetaRocq.Examples.metarocq_tour_prelude]
inhabit_formula [in MetaRocq.Examples.tauto]
init_graph [in MetaRocq.Common.uGraph]
inj_open [in MetaRocq.PCUIC.PCUICContextConversion]
inj_closed [in MetaRocq.PCUIC.PCUICContextConversion]
inj_tags [in MetaRocq.Erasure.EReorderCstrs]
inline [in MetaRocq.Erasure.EInlining]
inline [in MetaRocq.Erasure.Typed.CertifyingInlining]
inlined_program_inlinings [in MetaRocq.Erasure.EInlining]
inlined_program [in MetaRocq.Erasure.EInlining]
inline_transformation [in MetaRocq.Erasure.EInlining]
inline_program [in MetaRocq.Erasure.EInlining]
inline_env [in MetaRocq.Erasure.EInlining]
inline_add [in MetaRocq.Erasure.EInlining]
inline_decl [in MetaRocq.Erasure.EInlining]
inline_constant_decl [in MetaRocq.Erasure.EInlining]
inline_projections_optimization [in MetaRocq.ErasurePlugin.ETransform]
inline_def [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_globals_template [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_globals [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_in_decl [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_context_decl [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_oib [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_in_constant_body [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_aux [in MetaRocq.Erasure.Typed.CertifyingInlining]
inline_const [in MetaRocq.Erasure.Typed.CertifyingInlining]
inlining [in MetaRocq.Erasure.EInlining]
InPrim [in MetaRocq.Erasure.EPrimitive]
inspect [in MetaRocq.Examples.tauto]
inspect [in MetaRocq.SafeChecker.PCUICSafeReduce]
inspect [in MetaRocq.Erasure.ErasureFunction]
inspect [in MetaRocq.Erasure.EUnboxing]
inspect [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inspect_bool [in MetaRocq.Erasure.ErasureFunction]
inst [in MetaRocq.PCUIC.PCUICSigmaCalculus]
Instance.empty [in MetaRocq.Common.Universes]
Instance.eqb [in MetaRocq.Common.Universes]
Instance.equal_upto [in MetaRocq.Common.Universes]
Instance.is_empty [in MetaRocq.Common.Universes]
Instance.t [in MetaRocq.Common.Universes]
instantiated_sind [in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_rec [in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_ind [in MetaRocq.PCUIC.PCUICFirstorder]
instantiated_rect [in MetaRocq.PCUIC.PCUICFirstorder]
instantiate_params_subst [in MetaRocq.Template.Typing]
instantiate_params_subst_spec_sind [in MetaRocq.Template.Typing]
instantiate_params_subst_spec_ind [in MetaRocq.Template.Typing]
instantiate_cstr_indices [in MetaRocq.PCUIC.PCUICCasesHelper]
inst_mfix [in MetaRocq.PCUIC.PCUICGuardCondition]
inst_mutual_inductive_body [in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_context_snoc0 [in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_decl [in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_context [in MetaRocq.PCUIC.Syntax.PCUICInstDef]
inst_case_branch_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_predicate_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_context [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_telescope [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_constructor_body [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_context [in MetaRocq.Template.Ast]
inter_checker_flags [in MetaRocq.Common.config]
invert_Forall2_dep [in MetaRocq.Utils.All_Forall]
invert_Forall2 [in MetaRocq.Utils.All_Forall]
iota_body [in MetaRocq.Erasure.Typed.Utils]
iota_red [in MetaRocq.Template.Typing]
iota_red [in MetaRocq.PCUIC.Syntax.PCUICCases]
iota_red [in MetaRocq.Erasure.EGlobalEnv]
isApp [in MetaRocq.PCUIC.PCUICAst]
isApp [in MetaRocq.Erasure.EAst]
isApp [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
isApp [in MetaRocq.Template.Ast]
isAppPrim [in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppProd [in MetaRocq.PCUIC.PCUICSafeLemmata]
isArity [in MetaRocq.PCUIC.PCUICTyping]
isArity [in MetaRocq.Template.Typing]
isArityHead [in MetaRocq.Template.WcbvEval]
isArityHead [in MetaRocq.PCUIC.PCUICWcbvEval]
isAssRel [in MetaRocq.Template.WcbvEval]
isAssRel [in MetaRocq.PCUIC.PCUICWcbvEval]
isAxiom [in MetaRocq.Template.WcbvEval]
isAxiom [in MetaRocq.PCUIC.PCUICWcbvEval]
isBox [in MetaRocq.Erasure.EAstUtils]
isCoFinite [in MetaRocq.PCUIC.PCUICTyping]
isCoFinite [in MetaRocq.Template.Typing]
isCoFix [in MetaRocq.Template.WcbvEval]
isCoFix [in MetaRocq.Template.Checker]
isCoFix [in MetaRocq.PCUIC.PCUICWcbvEval]
isCoFix [in MetaRocq.Erasure.EAstUtils]
isCoFix_app [in MetaRocq.SafeChecker.PCUICSafeReduce]
isConstruct [in MetaRocq.Template.WcbvEval]
isConstruct [in MetaRocq.Template.EtaExpand]
isConstruct [in MetaRocq.PCUIC.PCUICEtaExpand]
isConstruct [in MetaRocq.Template.Checker]
isConstruct [in MetaRocq.PCUIC.PCUICWcbvEval]
isConstruct [in MetaRocq.Erasure.EAstUtils]
isConstructApp [in MetaRocq.Template.WcbvEval]
isConstructApp [in MetaRocq.PCUIC.PCUICWcbvEval]
isConstructApp [in MetaRocq.Erasure.EAstUtils]
isConstruct_app [in MetaRocq.Template.AstUtils]
isConstruct_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
isconv [in MetaRocq.Template.Checker]
isconv [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_prog [in MetaRocq.Template.Checker]
isconv_term [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_full [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_array_values [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_array_values_aux [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_predicate [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_predicate_params [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_predicate_params_aux [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_branches' [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_branches [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_context [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_context_aux [in MetaRocq.SafeChecker.PCUICSafeConversion]
isErasable [in MetaRocq.Erasure.Extract]
isErasable_Type [in MetaRocq.Erasure.EArities]
isEtaExp [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_env [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_decl [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_constant_decl [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_env [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_decl [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_constant_decl [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_fixapp [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app [in MetaRocq.Erasure.EEtaExpandedFix]
isEvar [in MetaRocq.Template.WcbvEval]
isEvar [in MetaRocq.PCUIC.PCUICWcbvEval]
isEvar [in MetaRocq.Erasure.EAstUtils]
isFinite [in MetaRocq.PCUIC.PCUICTyping]
isFinite [in MetaRocq.Template.Typing]
isFix [in MetaRocq.Template.WcbvEval]
isFix [in MetaRocq.Template.EtaExpand]
isFix [in MetaRocq.PCUIC.PCUICEtaExpand]
isFix [in MetaRocq.PCUIC.PCUICWcbvEval]
isFix [in MetaRocq.Erasure.EAstUtils]
isFixApp [in MetaRocq.Template.WcbvEval]
isFixApp [in MetaRocq.PCUIC.PCUICConversion]
isFixApp [in MetaRocq.PCUIC.PCUICWcbvEval]
isFixApp [in MetaRocq.Erasure.EAstUtils]
isFixLambda [in MetaRocq.PCUIC.Syntax.PCUICViews]
isFixLambda_app [in MetaRocq.PCUIC.Syntax.PCUICViews]
isFix_app [in MetaRocq.Template.EtaExpand]
isFunction [in MetaRocq.ErasurePlugin.ErasureCorrectness]
isInd [in MetaRocq.PCUIC.utils.PCUICAstUtils]
isInd [in MetaRocq.PCUIC.PCUICWcbvEval]
isIndConstructApp [in MetaRocq.PCUIC.PCUICConvCumInversion]
isLambda [in MetaRocq.PCUIC.PCUICAst]
isLambda [in MetaRocq.Erasure.EAst]
isLambda [in MetaRocq.Template.Ast]
isLazy [in MetaRocq.Erasure.EAstUtils]
isLazyApp [in MetaRocq.Erasure.EAstUtils]
isPrim [in MetaRocq.PCUIC.PCUICSafeLemmata]
isPrim [in MetaRocq.Template.WcbvEval]
isPrim [in MetaRocq.PCUIC.PCUICWcbvEval]
isPrim [in MetaRocq.Erasure.EAstUtils]
isPrimApp [in MetaRocq.PCUIC.PCUICWcbvEval]
isPrimApp [in MetaRocq.Erasure.EAstUtils]
isProd [in MetaRocq.PCUIC.utils.PCUICAstUtils]
isPropositional [in MetaRocq.PCUIC.PCUICFirstorder]
isPropositionalArity [in MetaRocq.PCUIC.PCUICFirstorder]
isprop_ind [in MetaRocq.Erasure.EOptimizePropDiscr]
isred [in MetaRocq.SafeChecker.PCUICSafeReduce]
isred_full [in MetaRocq.SafeChecker.PCUICSafeConversion]
isRel [in MetaRocq.Template.EtaExpand]
isRel [in MetaRocq.PCUIC.PCUICEtaExpand]
isRel [in MetaRocq.SafeChecker.PCUICSafeChecker]
isRel [in MetaRocq.Erasure.EAstUtils]
isRel_app [in MetaRocq.Template.EtaExpand]
isRel_n [in MetaRocq.SafeChecker.PCUICSafeChecker]
isSome [in MetaRocq.Erasure.EWellformed]
isSort [in MetaRocq.PCUIC.utils.PCUICAstUtils]
isSort [in MetaRocq.Template.Typing]
isStackApp [in MetaRocq.PCUIC.Syntax.PCUICPosition]
isStuckFix [in MetaRocq.Template.WcbvEval]
isStuckFix [in MetaRocq.Erasure.EWcbvEval]
isStuckFix [in MetaRocq.PCUIC.PCUICWcbvEval]
isStuckFix' [in MetaRocq.Erasure.EEtaExpandedFix]
isTT [in MetaRocq.Erasure.Typed.Erasure]
isType_welltyped [in MetaRocq.PCUIC.PCUICTyping]
isWfArity [in MetaRocq.PCUIC.PCUICTyping]
isws_cumul_pb_Fix [in MetaRocq.SafeChecker.PCUICSafeConversion]
isws_cumul_pb_fix_bodies [in MetaRocq.SafeChecker.PCUICSafeConversion]
isws_cumul_pb_fix_types [in MetaRocq.SafeChecker.PCUICSafeConversion]
is_arity [in MetaRocq.Erasure.Typed.Erasure]
is_sort [in MetaRocq.Erasure.Typed.Erasure]
Is_conv_to_Sort [in MetaRocq.Erasure.Typed.Erasure]
is_prod_or_sort [in MetaRocq.Erasure.Typed.Erasure]
is_leaf [in MetaRocq.Examples.tauto]
is_suffix [in MetaRocq.Utils.MRList]
is_prefix [in MetaRocq.Utils.MRList]
Is_proof [in MetaRocq.PCUIC.PCUICElimination]
is_empty_type_decl [in MetaRocq.Erasure.Typed.Extraction]
is_allowed_elimination [in MetaRocq.Common.Universes]
is_lSet [in MetaRocq.Common.Universes]
is_allowed_elimination_cuniv [in MetaRocq.Common.Universes]
is_propositional_or_set [in MetaRocq.Common.Universes]
is_declared_cstr_levels [in MetaRocq.Common.Universes]
is_fresh [in MetaRocq.Template.Pretty]
is_erasable [in MetaRocq.Erasure.ErasureFunction]
is_erasableb [in MetaRocq.Erasure.ErasureFunction]
is_arity [in MetaRocq.Erasure.ErasureFunction]
is_ind_app_head [in MetaRocq.Template.AstUtils]
is_empty [in MetaRocq.Template.AstUtils]
is_unboxable [in MetaRocq.Erasure.EUnboxing]
is_allowed_elimination_dec [in MetaRocq.Common.UniversesDec]
is_lSet_dec [in MetaRocq.Common.UniversesDec]
is_box_or_any [in MetaRocq.Erasure.Typed.Optimize]
is_expanded_env [in MetaRocq.Erasure.Typed.Optimize]
is_expanded [in MetaRocq.Erasure.Typed.Optimize]
is_expanded_aux [in MetaRocq.Erasure.Typed.Optimize]
is_dead [in MetaRocq.Erasure.Typed.Optimize]
is_ind_app_head [in MetaRocq.PCUIC.utils.PCUICAstUtils]
is_nil [in MetaRocq.Erasure.EEtaExpanded]
is_supermodule_of [in MetaRocq.Quotation.ToPCUIC.Init]
is_submodule_of [in MetaRocq.Quotation.ToPCUIC.Init]
is_open_case [in MetaRocq.PCUIC.PCUICConversion]
Is_conv_to_Arity [in MetaRocq.PCUIC.PCUICConversion]
is_fresh [in MetaRocq.PCUIC.utils.PCUICPretty]
is_eta_fix_app_map [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_app_map [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_vdef [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_application_sind [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_application_ind [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_application_sind [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_eta_fix_application_ind [in MetaRocq.ErasurePlugin.ErasureCorrectness]
is_cons [in MetaRocq.Erasure.EEtaExpandedFix]
is_nil [in MetaRocq.Erasure.EEtaExpandedFix]
is_supermodule_of [in MetaRocq.Quotation.ToTemplate.Init]
is_submodule_of [in MetaRocq.Quotation.ToTemplate.Init]
is_nil [in MetaRocq.Template.TemplateCheckWf]
is_constructor [in MetaRocq.Template.Typing]
is_graph_of_global_env_ext [in MetaRocq.Template.Checker]
is_none [in MetaRocq.Erasure.Typed.Certifying]
is_fresh [in MetaRocq.Erasure.EPretty]
is_nil [in MetaRocq.Erasure.EWellformed]
is_axiom_decl [in MetaRocq.Erasure.Extract]
is_monomorphic_cstr [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_constructor [in MetaRocq.PCUIC.Syntax.PCUICCases]
is_graph_of_uctx [in MetaRocq.Common.uGraph]
is_lt [in MetaRocq.Common.uGraph]
is_consistent [in MetaRocq.Common.uGraph]
is_nth_constructor_app_or_box [in MetaRocq.Erasure.EGlobalEnv]
is_constructor_app_or_box [in MetaRocq.Erasure.EGlobalEnv]
is_box [in MetaRocq.Erasure.EAstUtils]
iter [in MetaRocq.Erasure.ErasureFunction]
it_mkLambda_or_LetIn [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
| 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) |