| 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 (lemma)
identity_typing [in MetaRocq.Examples.typing_correctness]idsn_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn_lt [in MetaRocq.PCUIC.PCUICSigmaCalculus]
idsn_length [in MetaRocq.PCUIC.PCUICSigmaCalculus]
id_nth_spec [in MetaRocq.PCUIC.PCUICSigmaCalculus]
id_id [in MetaRocq.PCUIC.PCUICAst]
iff_is_true_eq_bool [in MetaRocq.Utils.MRUtils]
iff_ex [in MetaRocq.Utils.MRUtils]
iff_forall [in MetaRocq.Utils.MRUtils]
iff_reflect [in MetaRocq.SafeChecker.PCUICSafeConversion]
if_true_false [in MetaRocq.Utils.MRUtils]
IHup [in MetaRocq.PCUIC.PCUICInductives]
implement_box_eval [in MetaRocq.Erasure.EImplementBox]
implement_box_mkApps [in MetaRocq.Erasure.EImplementBox]
implement_box_env_extends [in MetaRocq.Erasure.EImplementBox]
implement_box_env_wf_glob [in MetaRocq.Erasure.EImplementBox]
implement_box_declared_constant [in MetaRocq.Erasure.EImplementBox]
implement_box_isLazyApp [in MetaRocq.Erasure.EImplementBox]
implement_box_isPrimApp [in MetaRocq.Erasure.EImplementBox]
implement_box_isConstructApp [in MetaRocq.Erasure.EImplementBox]
implement_box_nth [in MetaRocq.Erasure.EImplementBox]
implement_box_cunfold_cofix [in MetaRocq.Erasure.EImplementBox]
implement_box_cunfold_fix [in MetaRocq.Erasure.EImplementBox]
implement_box_cofix_subst [in MetaRocq.Erasure.EImplementBox]
implement_box_fix_subst [in MetaRocq.Erasure.EImplementBox]
implement_box_iota_red [in MetaRocq.Erasure.EImplementBox]
implement_box_substl [in MetaRocq.Erasure.EImplementBox]
implement_box_csubst [in MetaRocq.Erasure.EImplementBox]
implement_box_lift [in MetaRocq.Erasure.EImplementBox]
impredicative_product [in MetaRocq.Common.Universes]
impredicative_csort_product [in MetaRocq.Common.Universes]
InA_In_eq [in MetaRocq.Utils.MRList]
includes_deps_fold [in MetaRocq.Erasure.ErasureFunctionProperties]
includes_deps_union [in MetaRocq.Erasure.ErasureFunctionProperties]
includes_deps_equiv [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
incl_cs_trans [in MetaRocq.Common.Universes]
incl_cs_refl [in MetaRocq.Common.Universes]
incl_cs_refl [in MetaRocq.Erasure.ErasureFunctionProperties]
incl_cs_refl [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
inds_nth_error [in MetaRocq.PCUIC.PCUICInductiveInversion]
inds_is_open_terms [in MetaRocq.PCUIC.PCUICInductiveInversion]
inds_nth_error [in MetaRocq.Erasure.EArities]
inds_spec [in MetaRocq.PCUIC.Syntax.PCUICCases]
inds_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
inds_spec [in MetaRocq.Template.Ast]
inds_length [in MetaRocq.Template.Ast]
inductive_cumulative_indices_smash [in MetaRocq.SafeChecker.PCUICSafeRetyping]
inductive_cumulative_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
inductive_ind_ind_bodies_length [in MetaRocq.PCUIC.PCUICInductives]
inductive_isprop_and_pars_trans_env_debox_types [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
inductive_isprop_and_pars_trans_env_dearg_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
ind_projs_reorder [in MetaRocq.Erasure.EReorderCstrs]
ind_ctors_no_reorder [in MetaRocq.Erasure.EReorderCstrs]
ind_ctors_reorder [in MetaRocq.Erasure.EReorderCstrs]
ind_whnf_classification [in MetaRocq.PCUIC.PCUICClassification]
ind_whnf_classification' [in MetaRocq.PCUIC.PCUICClassification]
ind_predicate_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
ind_predicate_context_length [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
infering_prod_on_free_vars [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
infering_on_free_vars [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
infering_ind_infering [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_ind_ind' [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_ind_ind [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_prod_infering [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_prod_prod' [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_prod_prod [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_sort_infering [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_sort_sort [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_checking [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_unique' [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_unique [in MetaRocq.PCUIC.Bidirectional.BDUnique]
infering_ind_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_prod_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_sort_isType [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_sort_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infering_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
infer_irrel [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_as_sort_irrel [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_as_prod_irrel [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
init_graph_invariants [in MetaRocq.Common.uGraph]
InPrim_size [in MetaRocq.Erasure.EInduction]
InPrim_primProp [in MetaRocq.Erasure.EPrimitive]
inspect_nth_error_rename [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
instantiated_typing_spine_firstorder_spine [in MetaRocq.PCUIC.PCUICFirstorder]
instantiate_wf_subslet [in MetaRocq.PCUIC.PCUICInductiveInversion]
instantiate_subslet [in MetaRocq.PCUIC.PCUICInductiveInversion]
instantiate_minductive [in MetaRocq.PCUIC.PCUICContexts]
instantiate_params_substP [in MetaRocq.Template.Typing]
instantiate_inds [in MetaRocq.PCUIC.PCUICInductives]
inst_case_branch_context_eq [in MetaRocq.PCUIC.PCUICSR]
inst_case_branch_context_rename [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
inst_case_predicate_context_rename [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
inst_prim_type [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_convSpec [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_cumulSpec [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_case_branch_context_inst [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_case_predicate_context_inst [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_context_on_free_vars [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
inst_case_predicate_context_alpha_eq [in MetaRocq.PCUIC.PCUICInductiveInversion]
inst_case_predicate_context_eq [in MetaRocq.PCUIC.PCUICAlpha]
inst_closed [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
inst_extended_subst_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_assoc [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_rename_assoc [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_rename_assoc_n [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_mkApps [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_cofix [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_fix [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_letin [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_prod [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_lam [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_app [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_ext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
inst_case_branch_context_eq [in MetaRocq.PCUIC.PCUICCasesContexts]
inst_case_predicate_context_eq [in MetaRocq.PCUIC.PCUICCasesContexts]
inst_is_constructor [in MetaRocq.PCUIC.PCUICParallelReduction]
inst_ctxmap_up [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inst_ctxmap [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
inst_case_branch_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_predicate_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICConvCumInversion]
inst_case_branch_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_predicate_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_context_assumptions [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_case_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
inst_context_telescope [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_cons [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_upn0 [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst_telescope [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cumul_decls [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_conv_decls [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cumul [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_conv [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_is_open_term [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_on_free_vars [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_ext_cond [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_set_preturn [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_set_pparams [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_unfold_cofix [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_unfold_fix [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_iota_red [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_extended_subst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_cofixpoint [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_fixpoint [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_check_one_cofix [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_check_one_fix [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_smash_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_app_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_decompose_prod_assum [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_type [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_context_gen [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cstr_branch_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_inst_case_context_wf [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_inst_case_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_set_binder_name [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_inds [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_lift [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_lift [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed_extended_subst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closedn_terms [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_cstr_args [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed_constructor_body [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed_decl [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_branches [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_branch [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_predicate [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_predicate_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst_k [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_to_extended_list [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_reln [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_mkLambda_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_preturn [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_pcontext [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_fix_context_up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_fix_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_destArity [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_wf_local [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closedn_ctx [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_decl_closed [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_ext_closed [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_closed0 [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_subst0 [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_mkApps [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_length [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_alt [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_context_snoc [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_context_eq [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
inst_case_predicate_context_eq [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
inter_checker_flags_spec [in MetaRocq.Common.config]
into_closed_red_ctx [in MetaRocq.PCUIC.PCUICSR]
into_wt_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_decls [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_pb_terms_Algo [in MetaRocq.SafeChecker.PCUICSafeRetyping]
into_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICContextConversion]
into_ws_cumul_pb_terms [in MetaRocq.PCUIC.PCUICInductiveInversion]
into_ws_cumul_ctx_pb_rel [in MetaRocq.PCUIC.PCUICInductiveInversion]
into_closed_red [in MetaRocq.PCUIC.PCUICConversion]
into_ws_cumul [in MetaRocq.PCUIC.PCUICInversion]
into_red_terms [in MetaRocq.PCUIC.PCUICConvCumInversion]
introP [in MetaRocq.Utils.ReflectEq]
introT [in MetaRocq.Utils.MRReflect]
inversion_Rel [in MetaRocq.Examples.tauto]
inversion_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICSpine]
inversion_mkApps_direct [in MetaRocq.PCUIC.PCUICSpine]
inversion_mkApps [in MetaRocq.PCUIC.PCUICValidity]
inversion_it_mkProd_or_LetIn [in MetaRocq.SafeChecker.PCUICSafeChecker]
inversion_mkApps [in MetaRocq.PCUIC.PCUICProgress]
inversion_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICInversion]
inversion_Prim [in MetaRocq.PCUIC.PCUICInversion]
inversion_CoFix [in MetaRocq.PCUIC.PCUICInversion]
inversion_Fix [in MetaRocq.PCUIC.PCUICInversion]
inversion_Proj [in MetaRocq.PCUIC.PCUICInversion]
inversion_Case [in MetaRocq.PCUIC.PCUICInversion]
inversion_Construct [in MetaRocq.PCUIC.PCUICInversion]
inversion_Ind [in MetaRocq.PCUIC.PCUICInversion]
inversion_Const [in MetaRocq.PCUIC.PCUICInversion]
inversion_App_size [in MetaRocq.PCUIC.PCUICInversion]
inversion_App [in MetaRocq.PCUIC.PCUICInversion]
inversion_LetIn [in MetaRocq.PCUIC.PCUICInversion]
inversion_Lambda [in MetaRocq.PCUIC.PCUICInversion]
inversion_Prod_size [in MetaRocq.PCUIC.PCUICInversion]
inversion_Prod [in MetaRocq.PCUIC.PCUICInversion]
inversion_Sort [in MetaRocq.PCUIC.PCUICInversion]
inversion_Evar [in MetaRocq.PCUIC.PCUICInversion]
inversion_Var [in MetaRocq.PCUIC.PCUICInversion]
inversion_Rel [in MetaRocq.PCUIC.PCUICInversion]
invert_cumul_it_mkProd_or_LetIn_Sort_Ind [in MetaRocq.PCUIC.PCUICFirstorder]
invert_red_mkApps_tRel [in MetaRocq.PCUIC.PCUICInductiveInversion]
invert_Proj_Construct [in MetaRocq.PCUIC.PCUICInductiveInversion]
invert_Case_Construct [in MetaRocq.PCUIC.PCUICInductiveInversion]
invert_red_lambda [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_ind_sort [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_sort_ind [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_ind_ind [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_ind_prod [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_prod_ind [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_Prim [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_prim_type_prod [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_prim_type_ind [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_axiom_prod [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_axiom_ind [in MetaRocq.PCUIC.PCUICConversion]
invert_red_mkApps_tInd [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_arity_l [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_arity_r [in MetaRocq.PCUIC.PCUICConversion]
invert_red_sort [in MetaRocq.PCUIC.PCUICConversion]
invert_red_tPrim [in MetaRocq.PCUIC.PCUICConversion]
invert_red_axiom_app [in MetaRocq.PCUIC.PCUICConversion]
invert_red1_axiom_app [in MetaRocq.PCUIC.PCUICConversion]
invert_red_axiom [in MetaRocq.PCUIC.PCUICConversion]
invert_red_prod [in MetaRocq.PCUIC.PCUICConversion]
invert_red_letin [in MetaRocq.PCUIC.PCUICConversion]
invert_cumul_arity_l [in MetaRocq.PCUIC.PCUICArities]
invert_red1_letin [in MetaRocq.PCUIC.PCUICInductives]
invert_type_mkApps_ind [in MetaRocq.PCUIC.PCUICInductives]
invert_fix_ind [in MetaRocq.PCUIC.PCUICClassification]
invert_ind_ind [in MetaRocq.PCUIC.PCUICClassification]
invert_cumul_arity_r_gen [in MetaRocq.PCUIC.PCUICClassification]
invert_cumul_arity_l_gen [in MetaRocq.PCUIC.PCUICClassification]
invert_it_Ind_eq_prod [in MetaRocq.Erasure.EArities]
invert_type_mkApps_tProd [in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_opt_monad [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
inv_stuck_cofixes [in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_stuck_fixes [in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_reduced_body_proj [in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_reduced_discriminees_case [in MetaRocq.SafeChecker.PCUICSafeConversion]
inv_wf_local [in MetaRocq.SafeChecker.PCUICTypeChecker]
inv_opt_monad [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
inv_on_free_vars_decl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
In_app_inv [in MetaRocq.Erasure.Typed.Erasure]
In_size [in MetaRocq.Utils.MRList]
In_unfold_inj [in MetaRocq.Utils.MRList]
In_map [in MetaRocq.PCUIC.PCUICElimination]
in_global_deps_fresh [in MetaRocq.Erasure.ErasureFunction]
In_skipn [in MetaRocq.Erasure.ErasureFunction]
in_global_deps [in MetaRocq.Erasure.ErasureFunction]
in_global_levels [in MetaRocq.PCUIC.PCUICWeakeningEnv]
In_term_global_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
In_map_All [in MetaRocq.Erasure.ErasureFunctionProperties]
in_deps_in_erase_global_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
in_erase_global_deps_acc [in MetaRocq.Erasure.ErasureFunctionProperties]
In_lift_constraints [in MetaRocq.PCUIC.PCUICInductiveInversion]
In_Var_global_ext_poly [in MetaRocq.SafeChecker.PCUICSafeChecker]
In_unfold_inj [in MetaRocq.SafeChecker.PCUICSafeChecker]
In_list_depth [in MetaRocq.PCUIC.Syntax.PCUICDepth]
In_Forall [in MetaRocq.Utils.All_Forall]
In_All [in MetaRocq.Utils.All_Forall]
In_lookup_globals [in MetaRocq.Template.TypingWf]
in_global_ext_subst_abs_level [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
in_var_global_ext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance_cstrs' [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance_cstrs [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_unfold_var [in MetaRocq.PCUIC.PCUICWfUniverses]
in_subst_instance [in MetaRocq.PCUIC.PCUICWfUniverses]
In_Level_global_ext_poly [in MetaRocq.PCUIC.PCUICWfUniverses]
iota_red_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
irred_equal [in MetaRocq.PCUIC.PCUICNormalization]
isAppPrim_isPrim [in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppPrim_mkApps [in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppProd_isProd [in MetaRocq.PCUIC.PCUICSafeLemmata]
isAppProd_mkApps [in MetaRocq.PCUIC.PCUICSafeLemmata]
isApp_false_nApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
isApp_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
isApp_mkApps [in MetaRocq.Erasure.ERemoveParams]
isArityHead_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isArity_mkNormalArity [in MetaRocq.Erasure.Typed.Erasure]
isArity_red [in MetaRocq.Erasure.Typed.Erasure]
isArity_red [in MetaRocq.SafeChecker.PCUICSafeReduce]
isArity_mkAssumArity [in MetaRocq.SafeChecker.PCUICSafeReduce]
isArity_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isArity_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isArity_red1 [in MetaRocq.PCUIC.PCUICConversion]
isArity_subst [in MetaRocq.PCUIC.PCUICConversion]
isArity_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICArities]
isArity_ind [in MetaRocq.PCUIC.PCUICClassification]
isArity_typing_spine [in MetaRocq.PCUIC.PCUICClassification]
isArity_subst [in MetaRocq.PCUIC.PCUICClassification]
isArity_mkApps [in MetaRocq.Erasure.EArities]
isArity_ind_type [in MetaRocq.Erasure.EArities]
isBox_csubst [in MetaRocq.Erasure.ECSubst]
isBox_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
isBox_optimize [in MetaRocq.Erasure.EReorderCstrs]
isBox_mkApps [in MetaRocq.Erasure.EWcbvEval]
isBox_optimize [in MetaRocq.Erasure.EInlineProjections]
isBox_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isBox_mkApps_Construct [in MetaRocq.Erasure.ERemoveParams]
isBox_mkApps' [in MetaRocq.Erasure.ERemoveParams]
isBox_lift [in MetaRocq.Erasure.ELiftSubst]
isBox_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
isConstructApp_mkApps [in MetaRocq.Template.WcbvEval]
isConstructApp_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isConstructApp_mkApps [in MetaRocq.PCUIC.PCUICWcbvEval]
isConstructApp_mkApps [in MetaRocq.Erasure.EAstUtils]
isConstruct_app_ne [in MetaRocq.PCUIC.PCUICNormal]
isConstruct_app_eq_term_r [in MetaRocq.PCUIC.PCUICEquality]
isConstruct_app_eq_term_l [in MetaRocq.PCUIC.PCUICEquality]
isConstruct_erase [in MetaRocq.Erasure.ErasureFunctionProperties]
isConstruct_app_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
isConstruct_app_pred1 [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
isConstruct_app_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
isConstruct_app_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
isconv_term_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_term_sound [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
isconv_sound [in MetaRocq.SafeChecker.PCUICSafeConversion]
isErasable_subst_instance [in MetaRocq.Erasure.ErasureProperties]
isErasable_irrel_global_env [in MetaRocq.Erasure.ErasureFunctionProperties]
isErasable_lets [in MetaRocq.ErasurePlugin.ErasureCorrectness]
isErasable_red [in MetaRocq.Erasure.EArities]
isErasable_unfold_cofix [in MetaRocq.Erasure.EArities]
isErasable_Propositional [in MetaRocq.Erasure.EArities]
isErasable_any_type [in MetaRocq.Erasure.EArities]
isErasable_Proof [in MetaRocq.Erasure.EArities]
isEtaExpFix_env_isEtaExp_env [in MetaRocq.Erasure.EEtaExpanded]
isEtaExpFix_isEtaExp [in MetaRocq.Erasure.EEtaExpanded]
isEtaExpFix_tApp_arg [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps [in MetaRocq.Erasure.EUnboxing]
isEtaExp_tApp_arg [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_env_expanded_global_env [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_expanded [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app_expanded [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_lookup [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_extends_decl [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_extends [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app_extends [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_lookup_ext [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_cunfold_cofix [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_cunfold_fix [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_cofix_subst [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_fix_subst [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_iota_red [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_substl [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_intro [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_app_mon [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_tApp [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_intro_notConstruct [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_Constructor [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_napp [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_mkApps_nonnil [in MetaRocq.Erasure.EEtaExpanded]
isEtaExp_lift [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_iota_red' [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_closedn [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tApp_eval [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tFix [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_FixApp [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_fixapp_mon [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_lookup [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_extends_decl [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_extends [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app_extends [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_lookup_ext [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tApp' [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_expanded [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app_expanded [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_tApp [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_cunfold_cofix [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_cunfold_fix [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_cofix_subst [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_iota_red [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_fixsubstl [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_substl [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_closed [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps_intro [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_Constructor [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps_nonnil [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_app_mon [in MetaRocq.Erasure.EEtaExpandedFix]
isEtaExp_dearg_single_construct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_dearg_single [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_dearg_lambdas [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_dearg_case_branch_body_rec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isEtaExp_mkApps [in MetaRocq.Erasure.ERemoveParams]
isFixApp_mkApps [in MetaRocq.Template.WcbvEval]
isFixApp_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isFixApp_trans [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isFixApp_mkApps [in MetaRocq.PCUIC.PCUICConversion]
isFixApp_mkApps [in MetaRocq.PCUIC.PCUICWcbvEval]
isFixApp_mkApps [in MetaRocq.Erasure.EAstUtils]
isFixLambda_app_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
isFixLambda_app_mkApps' [in MetaRocq.PCUIC.Syntax.PCUICViews]
isFixLambda_app_mkApps [in MetaRocq.PCUIC.Syntax.PCUICViews]
isFix_mkApps [in MetaRocq.Erasure.EGenericGlobalMap]
isFix_mkApps [in MetaRocq.Erasure.EEtaExpandedFix]
isFix_mkApps [in MetaRocq.Erasure.EOptimizePropDiscr]
isFix_mkApps [in MetaRocq.Erasure.EGenericMapEnv]
isFix_mkApps [in MetaRocq.Erasure.EReorderCstrs]
isFix_mkApps [in MetaRocq.Erasure.EInlineProjections]
isFix_mkApps_Construct [in MetaRocq.Erasure.ERemoveParams]
isFix_mkApps' [in MetaRocq.Erasure.ERemoveParams]
isFix_mkApps [in MetaRocq.Erasure.ECoInductiveToInductive]
isIndConstructApp_mkApps [in MetaRocq.PCUIC.PCUICConvCumInversion]
isLambda_eq_term_r [in MetaRocq.PCUIC.PCUICEquality]
isLambda_eq_term_l [in MetaRocq.PCUIC.PCUICEquality]
isLambda_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
isLambda_lift [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
isLambda_implement_box [in MetaRocq.Erasure.EImplementBox]
isLambda_subst_instance [in MetaRocq.Erasure.ErasureProperties]
isLambda_csubst [in MetaRocq.Erasure.ECSubst]
isLambda_inv [in MetaRocq.Erasure.ErasureFunctionProperties]
isLambda_eta_expand [in MetaRocq.Template.EtaExpand]
isLambda_unlift [in MetaRocq.Template.EtaExpand]
isLambda_subst [in MetaRocq.Template.LiftSubst]
isLambda_lift [in MetaRocq.Template.LiftSubst]
isLambda_red1 [in MetaRocq.PCUIC.PCUICInductiveInversion]
isLambda_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isLambda_isApp [in MetaRocq.Template.WfAst]
isLambda_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
isLambda_inv [in MetaRocq.PCUIC.PCUICAst]
isLambda_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
isLambda_optimize [in MetaRocq.Erasure.EReorderCstrs]
isLambda_transform_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
isLambda_mkApps [in MetaRocq.Erasure.EWcbvEval]
isLambda_optimize [in MetaRocq.Erasure.EInlineProjections]
isLambda_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
isLambda_mkApps_Construct [in MetaRocq.Erasure.ERemoveParams]
isLambda_mkApps' [in MetaRocq.Erasure.ERemoveParams]
isLambda_subst [in MetaRocq.Erasure.ELiftSubst]
isLambda_lift [in MetaRocq.Erasure.ELiftSubst]
isLambda_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
isLazyApp_mkApps [in MetaRocq.Erasure.EAstUtils]
isPrimApp_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isPrimApp_mkApps [in MetaRocq.PCUIC.PCUICWcbvEval]
isPrimApp_mkApps [in MetaRocq.Erasure.EAstUtils]
isPrimmkApps [in MetaRocq.PCUIC.PCUICSafeLemmata]
isPrim_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
isProdmkApps [in MetaRocq.PCUIC.PCUICSafeLemmata]
isPropositional_propositional_cstr [in MetaRocq.Erasure.EArities]
isPropositional_propositional [in MetaRocq.Erasure.EArities]
isred_full_nobeta [in MetaRocq.SafeChecker.PCUICSafeConversion]
isSortmkApps [in MetaRocq.PCUIC.PCUICSafeLemmata]
isStackApp_false_appstack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
isStuckfix_nApp [in MetaRocq.Template.WcbvEval]
isStuckfix_nApp [in MetaRocq.Erasure.EWcbvEval]
isStuckfix_nApp [in MetaRocq.PCUIC.PCUICWcbvEval]
isTypebd_isType [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
isType_prod_cod [in MetaRocq.Erasure.Typed.Erasure]
isType_prod_dom [in MetaRocq.Erasure.Typed.Erasure]
isType_red_sq [in MetaRocq.Erasure.Typed.Erasure]
isType_tLetIn [in MetaRocq.PCUIC.PCUICSR]
isType_red [in MetaRocq.PCUIC.PCUICSR]
isType_red1 [in MetaRocq.PCUIC.PCUICSR]
isType_mkApps_Ind_proj_inv [in MetaRocq.PCUIC.PCUICSR]
isType_subst_extended_subst [in MetaRocq.PCUIC.PCUICSR]
isType_expand_lets [in MetaRocq.PCUIC.PCUICSR]
isType_subst_arities [in MetaRocq.PCUIC.PCUICSR]
isType_weaken [in MetaRocq.PCUIC.PCUICSR]
isType_lift [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
isType_substitution [in MetaRocq.PCUIC.PCUICSubstitution]
isType_closedPT [in MetaRocq.PCUIC.PCUICSubstitution]
isType_wf_local [in MetaRocq.PCUIC.PCUICSubstitution]
isType_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICElimination]
isType_it_mkProd_or_LetIn_app [in MetaRocq.PCUIC.PCUICSpine]
isType_context_conversion [in MetaRocq.PCUIC.PCUICFirstorder]
isType_ws_cumul_pb_refl [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
isType_open [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
isType_weakening [in MetaRocq.PCUIC.PCUICValidity]
isType_subst_instance_decl [in MetaRocq.PCUIC.PCUICValidity]
isType_Sort_inv [in MetaRocq.PCUIC.PCUICValidity]
isType_extends [in MetaRocq.PCUIC.PCUICValidity]
isType_weaken_full [in MetaRocq.PCUIC.PCUICValidity]
isType_wt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
isType_subst_instance_id [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isType_subst_instance_decl [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isType_all_rels_subst_lift [in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_subst_all_rels [in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_is_open_term [in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_mkApps_Ind_smash [in MetaRocq.PCUIC.PCUICInductiveInversion]
isType_weaken [in MetaRocq.PCUIC.PCUICArities]
isType_it_mkProd_or_LetIn_wf_local [in MetaRocq.PCUIC.PCUICArities]
isType_substitution_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICArities]
isType_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICArities]
isType_apply [in MetaRocq.PCUIC.PCUICArities]
isType_tLetIn_dom [in MetaRocq.PCUIC.PCUICArities]
isType_tLetIn_red [in MetaRocq.PCUIC.PCUICArities]
isType_subst_gen [in MetaRocq.PCUIC.PCUICArities]
isType_subst [in MetaRocq.PCUIC.PCUICArities]
isType_tProd [in MetaRocq.PCUIC.PCUICArities]
isType_Sort [in MetaRocq.PCUIC.PCUICArities]
isType_alpha_ctx [in MetaRocq.PCUIC.PCUICAlpha]
isType_alpha [in MetaRocq.PCUIC.PCUICAlpha]
isType_eq_context_conversion [in MetaRocq.PCUIC.PCUICAlpha]
isType_it_mkProd [in MetaRocq.Erasure.EOptimizePropDiscr]
isType_tSort [in MetaRocq.Erasure.EOptimizePropDiscr]
isType_mkApps_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
isType_it_mkProd_or_LetIn_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
isType_infering_sort [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
isType_case_predicate [in MetaRocq.PCUIC.PCUICInductives]
isType_mkApps_Ind_inv' [in MetaRocq.PCUIC.PCUICInductives]
isType_mkApps_Ind_inv [in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_subst [in MetaRocq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_inv [in MetaRocq.PCUIC.PCUICInductives]
isType_mkApps_Ind [in MetaRocq.PCUIC.PCUICInductives]
isType_intro [in MetaRocq.PCUIC.PCUICInductives]
isType_on_ctx_free_vars [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
isType_on_free_vars [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
isType_closed_red_refl [in MetaRocq.Erasure.EArities]
isType_red [in MetaRocq.Erasure.EArities]
isType_isErasable [in MetaRocq.Erasure.EArities]
isType_wf_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
isType_mkApps_Ind_smash_inv [in MetaRocq.SafeChecker.PCUICTypeChecker]
isType_mkApps_Ind_smash [in MetaRocq.SafeChecker.PCUICTypeChecker]
isType_wt [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
isType_mkApps_Ind_inv_spine [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
isType_is_open_term [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
isType_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
isType_mkApps_Ind_inv_spine [in MetaRocq.PCUIC.PCUICCasesHelper]
isType_lift [in MetaRocq.PCUIC.PCUICCasesHelper]
isType_it_mkProd [in MetaRocq.Erasure.ECoInductiveToInductive]
isType_tSort [in MetaRocq.Erasure.ECoInductiveToInductive]
isWfArity_red [in MetaRocq.PCUIC.PCUICSR]
isWfArity_red1 [in MetaRocq.PCUIC.PCUICSR]
isWfArity_subst_instance_decl [in MetaRocq.PCUIC.PCUICValidity]
isWfArity_alpha [in MetaRocq.PCUIC.PCUICAlpha]
isWfArity_prod_inv [in MetaRocq.Erasure.EArities]
isWfArity_sort [in MetaRocq.PCUIC.PCUICPrincipality]
is_constructor_app_false [in MetaRocq.PCUIC.PCUICNormal]
Is_conv_to_Arity_conv_arity [in MetaRocq.Erasure.Typed.Erasure]
is_open_term_snoc [in MetaRocq.PCUIC.PCUICSR]
is_closed_context_set_binder_name [in MetaRocq.PCUIC.PCUICSR]
is_assumption_context_spec [in MetaRocq.Erasure.Prelim]
is_leaf_sound [in MetaRocq.Examples.tauto]
Is_conv_to_Arity_red [in MetaRocq.SafeChecker.PCUICSafeReduce]
is_prefix_rev_is_suffix [in MetaRocq.Utils.MRList]
is_suffix_is_prefix_rev [in MetaRocq.Utils.MRList]
is_prefix_cons_inv [in MetaRocq.Utils.MRList]
is_prefix_cons [in MetaRocq.Utils.MRList]
is_prefix_nil [in MetaRocq.Utils.MRList]
Is_proof_mkApps_tConstruct [in MetaRocq.PCUIC.PCUICElimination]
is_propositional_subst_instance [in MetaRocq.PCUIC.PCUICElimination]
is_allowed_elimination_monotone [in MetaRocq.Common.Universes]
is_sprop_sort_prod [in MetaRocq.Common.Universes]
is_prop_sort_prod [in MetaRocq.Common.Universes]
is_type_sup_r [in MetaRocq.Common.Universes]
is_sprop_sup_iff [in MetaRocq.Common.Universes]
is_prop_sup [in MetaRocq.Common.Universes]
is_prop_or_sprop_sort_sup_prop [in MetaRocq.Common.Universes]
is_prop_sort_sup_prop [in MetaRocq.Common.Universes]
is_prop_or_sprop_sort_sup [in MetaRocq.Common.Universes]
is_prop_sort_sup' [in MetaRocq.Common.Universes]
is_prop_sort_sup [in MetaRocq.Common.Universes]
is_not_prop_and_is_not_sprop [in MetaRocq.Common.Universes]
is_prop_and_is_sprop_val_false [in MetaRocq.Common.Universes]
is_sprop_val [in MetaRocq.Common.Universes]
is_prop_val [in MetaRocq.Common.Universes]
is_closed_context_smash_end [in MetaRocq.PCUIC.PCUICSpine]
is_erasableb_irrel_global_env [in MetaRocq.Erasure.ErasureFunction]
is_arity_irrel [in MetaRocq.Erasure.ErasureFunction]
is_erasableb_irrel [in MetaRocq.Erasure.ErasureFunction]
is_erasableP [in MetaRocq.Erasure.ErasureFunction]
is_arityP [in MetaRocq.Erasure.ErasureFunction]
is_ind_app_head_mkApps [in MetaRocq.Template.AstUtils]
is_empty_app [in MetaRocq.Template.AstUtils]
Is_type_conv_context [in MetaRocq.Erasure.ErasureProperties]
is_PrimApp_erases [in MetaRocq.Erasure.ErasureProperties]
is_ConstructApp_erases [in MetaRocq.Erasure.ErasureProperties]
is_FixApp_erases [in MetaRocq.Erasure.ErasureProperties]
is_propositional_cstr_unbox [in MetaRocq.Erasure.EUnboxing]
is_propositional_unbox [in MetaRocq.Erasure.EUnboxing]
is_nil [in MetaRocq.Template.WcbvEval]
is_ind_app_head_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
is_closed_context_cumul_app [in MetaRocq.PCUIC.PCUICContextConversion]
is_closed_context_cstr_branch_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
is_closed_context_subst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
is_assumption_context_spec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
is_propositional_cstr_gen_transform [in MetaRocq.Erasure.EGenericGlobalMap]
is_propositional_gen_transform [in MetaRocq.Erasure.EGenericGlobalMap]
is_closed_context_weaken [in MetaRocq.PCUIC.PCUICInductiveInversion]
is_closed_subst_inst [in MetaRocq.PCUIC.PCUICInductiveInversion]
is_open_term_subst_instance [in MetaRocq.PCUIC.PCUICConversion]
is_closed_context_subst_instance [in MetaRocq.PCUIC.PCUICConversion]
is_open_term_lift [in MetaRocq.PCUIC.PCUICConversion]
is_closed_context_lift [in MetaRocq.PCUIC.PCUICConversion]
is_open_fix_onone2 [in MetaRocq.PCUIC.PCUICConversion]
is_open_fix_or_cofix [in MetaRocq.PCUIC.PCUICConversion]
is_open_brs_OnOne2 [in MetaRocq.PCUIC.PCUICConversion]
is_open_case_set_preturn [in MetaRocq.PCUIC.PCUICConversion]
is_open_case_set_pparams [in MetaRocq.PCUIC.PCUICConversion]
is_open_case_split [in MetaRocq.PCUIC.PCUICConversion]
Is_conv_to_Arity_inv [in MetaRocq.PCUIC.PCUICConversion]
is_open_term_subst [in MetaRocq.PCUIC.PCUICConversion]
is_open_term_subst_gen [in MetaRocq.PCUIC.PCUICConversion]
is_closed_subst_context [in MetaRocq.PCUIC.PCUICConversion]
is_closed_context_app_right [in MetaRocq.PCUIC.PCUICAlpha]
is_closed_context_app_left [in MetaRocq.PCUIC.PCUICAlpha]
is_constructor_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
is_type_subst [in MetaRocq.Erasure.ESubstitution]
Is_type_weakening [in MetaRocq.Erasure.ESubstitution]
Is_proof_extends [in MetaRocq.Erasure.ESubstitution]
Is_type_extends [in MetaRocq.Erasure.ESubstitution]
is_propositional_cstr_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
is_propositional_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
is_box_inv [in MetaRocq.Erasure.EOptimizePropDiscr]
is_propositional_cstr_gen_transform [in MetaRocq.Erasure.EGenericMapEnv]
is_propositional_gen_transform [in MetaRocq.Erasure.EGenericMapEnv]
is_propositional_cstr_optimize [in MetaRocq.Erasure.EReorderCstrs]
is_propositional_optimize [in MetaRocq.Erasure.EReorderCstrs]
is_closed_context_expand_let [in MetaRocq.PCUIC.PCUICInductives]
is_closed_context_weaken [in MetaRocq.PCUIC.PCUICCumulProp]
is_closed_context_snoc_inv [in MetaRocq.PCUIC.PCUICCumulProp]
is_sprop_prod [in MetaRocq.PCUIC.PCUICCumulProp]
is_prop_prod [in MetaRocq.PCUIC.PCUICCumulProp]
is_sprop_superE [in MetaRocq.PCUIC.PCUICCumulProp]
is_prop_superE [in MetaRocq.PCUIC.PCUICCumulProp]
is_sprop_bottom [in MetaRocq.PCUIC.PCUICCumulProp]
is_prop_bottom [in MetaRocq.PCUIC.PCUICCumulProp]
is_propositional_bottom [in MetaRocq.PCUIC.PCUICCumulProp]
is_constructor_pred1 [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
is_propositional_cstr_optimize [in MetaRocq.Erasure.EInlineProjections]
is_propositional_optimize [in MetaRocq.Erasure.EInlineProjections]
Is_conv_to_Arity_ind [in MetaRocq.PCUIC.PCUICClassification]
is_allowed_elimination_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_prop_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_sprop_subst_instance_univ [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_prop_subst_instance_univ [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_propositional_subst_instance_univ [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Is_proof_app [in MetaRocq.Erasure.EArities]
Is_proof_ind [in MetaRocq.Erasure.EArities]
is_propositional_lower [in MetaRocq.Erasure.EArities]
is_propositional_bottom [in MetaRocq.Erasure.EArities]
is_propositional_bottom' [in MetaRocq.Erasure.EArities]
Is_proof_ty [in MetaRocq.Erasure.EArities]
Is_type_eval_inv [in MetaRocq.Erasure.EArities]
Is_type_eval [in MetaRocq.Erasure.EArities]
Is_type_red [in MetaRocq.Erasure.EArities]
Is_type_lambda [in MetaRocq.Erasure.EArities]
is_propositional_sort_prod [in MetaRocq.Erasure.EArities]
Is_type_app [in MetaRocq.Erasure.EArities]
is_expanded_constant [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_cunfold_cofix [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_cunfold_fix [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_substl [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_csubst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_upwards [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_mkApps_inv [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_mkApps_eq [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_mkApps_eq [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_case [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_branch_body [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_lambdas [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_dearg_single [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_expanded_aux_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_subst_other [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_lift_all [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_lift_other [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_csubst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_dead_closed [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
is_constructor_prefix [in MetaRocq.PCUIC.Syntax.PCUICCases]
is_constructor_app_ge [in MetaRocq.PCUIC.Syntax.PCUICCases]
is_consistent_spec2 [in MetaRocq.Common.uGraph]
is_graph_of_uctx_add [in MetaRocq.Common.uGraph]
is_graph_of_uctx_levels [in MetaRocq.Common.uGraph]
is_lt_spec [in MetaRocq.Common.uGraph]
is_consistent_spec [in MetaRocq.Common.uGraph]
is_constructor_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
is_propositional_cstr_strip [in MetaRocq.Erasure.ERemoveParams]
is_propositional_strip [in MetaRocq.Erasure.ERemoveParams]
is_closed_ctx_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
is_open_term_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
is_graph_of_uctx_levels [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
is_propositional_cstr_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
is_propositional_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
is_box_inv [in MetaRocq.Erasure.ECoInductiveToInductive]
is_box_tApp [in MetaRocq.Erasure.EAstUtils]
is_box_mkApps [in MetaRocq.Erasure.EAstUtils]
iter_abstract_pop_decls_correct [in MetaRocq.Erasure.ErasureFunctionProperties]
it_mkProd_or_LetIn_inj [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
it_mkLambda_or_LetIn_inj [in MetaRocq.PCUIC.PCUICSafeLemmata]
it_mkLambda_or_LetIn_welltyped [in MetaRocq.PCUIC.PCUICSafeLemmata]
it_mkLambda_or_LetIn_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
it_mkProd_or_LetIn_wf_local [in MetaRocq.PCUIC.PCUICArities]
it_mkProd_or_LetIn_inj [in MetaRocq.Template.TypingWf]
it_mkProd_red_Arity [in MetaRocq.Erasure.EArities]
it_mkProd_arity [in MetaRocq.Erasure.EArities]
it_mkProd_isArity [in MetaRocq.Erasure.EArities]
it_mkLambda_or_LetIn_app [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
| 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) |