| 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) |
E (lemma)
ecofix_subst_nth [in MetaRocq.Erasure.Prelim]efix_subst_nth [in MetaRocq.Erasure.Prelim]
einfering_sort_isType [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
elimP [in MetaRocq.Utils.ReflectEq]
elimT [in MetaRocq.Utils.MRReflect]
elim_restriction_works_proj [in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works_proj_kelim1 [in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works [in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works_kelim [in MetaRocq.PCUIC.PCUICElimination]
elim_sort_intype [in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works_kelim1 [in MetaRocq.PCUIC.PCUICElimination]
elim_inspect [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
elookup_env_cons_disc [in MetaRocq.Erasure.ErasureFunctionProperties]
elookup_env_cons_fresh [in MetaRocq.Erasure.EGlobalEnv]
emkApps_snoc [in MetaRocq.Erasure.Prelim]
empty_contextset_subset [in MetaRocq.Common.Universes]
enumerate_unique [in MetaRocq.Utils.MRListable]
EnvironmentReflect.compatibleP [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_spec [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_globals_spec [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_globalsP [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extendsT [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_strictly_on_decls_spec [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_decls_spec [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_spec [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_strictly_on_declsT [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_declsT [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_decls_partT [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_decls_spec [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_declsT [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_decls_partT [in MetaRocq.Common.EnvironmentReflect]
Environment.All_decls_to_alpha [in MetaRocq.Common.Environment]
Environment.All_decls_alpha_impl [in MetaRocq.Common.Environment]
Environment.All_decls_impl [in MetaRocq.Common.Environment]
Environment.arities_context_length [in MetaRocq.Common.Environment]
Environment.context_assumptions_lift_context [in MetaRocq.Common.Environment]
Environment.context_assumptions_subst_context [in MetaRocq.Common.Environment]
Environment.context_assumptions_subst_instance [in MetaRocq.Common.Environment]
Environment.context_assumptions_mapi [in MetaRocq.Common.Environment]
Environment.context_assumptions_rev [in MetaRocq.Common.Environment]
Environment.context_assumptions_app [in MetaRocq.Common.Environment]
Environment.context_assumptions_map [in MetaRocq.Common.Environment]
Environment.context_assumptions_length_bound [in MetaRocq.Common.Environment]
Environment.context_assumptions_fold [in MetaRocq.Common.Environment]
Environment.declared_kername_set_mem_iff [in MetaRocq.Common.Environment]
Environment.declared_kername_set_spec [in MetaRocq.Common.Environment]
Environment.eta_global_env [in MetaRocq.Common.Environment]
Environment.expand_lets_ctx_length [in MetaRocq.Common.Environment]
Environment.expand_lets_k_ctx_length [in MetaRocq.Common.Environment]
Environment.extended_subst_length [in MetaRocq.Common.Environment]
Environment.extends_r_merge [in MetaRocq.Common.Environment]
Environment.extends_r_merge_globals [in MetaRocq.Common.Environment]
Environment.extends_l_merge [in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_l_merge [in MetaRocq.Common.Environment]
Environment.extends_l_merge_globals [in MetaRocq.Common.Environment]
Environment.extends_decls_part_trans [in MetaRocq.Common.Environment]
Environment.extends_decls_part_globals_trans [in MetaRocq.Common.Environment]
Environment.extends_decls_part_refl [in MetaRocq.Common.Environment]
Environment.extends_decls_part_globals_refl [in MetaRocq.Common.Environment]
Environment.extends_refl [in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_refl [in MetaRocq.Common.Environment]
Environment.hd_error_lookup_globals [in MetaRocq.Common.Environment]
Environment.ind_projs_map [in MetaRocq.Common.Environment]
Environment.ind_pars_map [in MetaRocq.Common.Environment]
Environment.ind_ctors_map [in MetaRocq.Common.Environment]
Environment.ind_type_map [in MetaRocq.Common.Environment]
Environment.it_mkProd_or_LetIn_app [in MetaRocq.Common.Environment]
Environment.lift_context_length [in MetaRocq.Common.Environment]
Environment.lift_context_alt [in MetaRocq.Common.Environment]
Environment.lookup_globals_filter [in MetaRocq.Common.Environment]
Environment.lookup_globals_app [in MetaRocq.Common.Environment]
Environment.lookup_env_extends_NoDup [in MetaRocq.Common.Environment]
Environment.lookup_global_extends_NoDup [in MetaRocq.Common.Environment]
Environment.lookup_global_Some_iff_In_NoDup [in MetaRocq.Common.Environment]
Environment.lookup_global_Some_if_In [in MetaRocq.Common.Environment]
Environment.lookup_globals_In [in MetaRocq.Common.Environment]
Environment.lookup_globals_nil [in MetaRocq.Common.Environment]
Environment.lookup_global_None [in MetaRocq.Common.Environment]
Environment.map_cst_body [in MetaRocq.Common.Environment]
Environment.map_cst_type [in MetaRocq.Common.Environment]
Environment.NoDup_lookup_globals_eq [in MetaRocq.Common.Environment]
Environment.NoDup_length_lookup_globals [in MetaRocq.Common.Environment]
Environment.nth_error_lt [in MetaRocq.Common.Environment]
Environment.nth_error_ge [in MetaRocq.Common.Environment]
Environment.nth_error_fold_context_k_eq [in MetaRocq.Common.Environment]
Environment.nth_error_fold_context_k [in MetaRocq.Common.Environment]
Environment.projs_length [in MetaRocq.Common.Environment]
Environment.reln_alt_eq [in MetaRocq.Common.Environment]
Environment.reln_list_lift_above [in MetaRocq.Common.Environment]
Environment.reln_fold [in MetaRocq.Common.Environment]
Environment.smash_context_app [in MetaRocq.Common.Environment]
Environment.smash_context_length [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_l_merge_globals [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_trans [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_globals_trans [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_refl [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_globals_refl [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_part [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_part_globals [in MetaRocq.Common.Environment]
Environment.subst_instance_length [in MetaRocq.Common.Environment]
Environment.subst_context_snoc [in MetaRocq.Common.Environment]
Environment.subst_context_alt [in MetaRocq.Common.Environment]
Environment.subst_context_nil [in MetaRocq.Common.Environment]
Environment.subst_context_length [in MetaRocq.Common.Environment]
Environment.to_extended_list_k_cons [in MetaRocq.Common.Environment]
Environment.to_extended_list_lift_above [in MetaRocq.Common.Environment]
Environment.to_extended_list_k_spec [in MetaRocq.Common.Environment]
EnvMap.fold_left_cons [in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_iff_NoDup [in MetaRocq.Common.EnvMap]
EnvMap.fresh_global_iff_not_In [in MetaRocq.Common.EnvMap]
EnvMap.gso [in MetaRocq.Common.EnvMap]
EnvMap.gss [in MetaRocq.Common.EnvMap]
EnvMap.lookup_spec [in MetaRocq.Common.EnvMap]
EnvMap.lookup_add_other [in MetaRocq.Common.EnvMap]
EnvMap.lookup_add [in MetaRocq.Common.EnvMap]
EnvMap.of_global_env_cons [in MetaRocq.Common.EnvMap]
EnvMap.remove_add_o [in MetaRocq.Common.EnvMap]
EnvMap.remove_add_eq [in MetaRocq.Common.EnvMap]
EnvMap.repr_add [in MetaRocq.Common.EnvMap]
EnvMap.repr_global_env [in MetaRocq.Common.EnvMap]
EnvMap.unfold_equal [in MetaRocq.Common.EnvMap]
EnvTyping.All_local_env_size_app [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size_pos [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_2 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_2 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_lift_prod_inv [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_prod_inv [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_app [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_app [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_app_inv [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_app_rel [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_local_rel [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_local [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_cst [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_nth_error [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_app_skipn [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_skipn [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_impl_ind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_impl_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_fold [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_map [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_ind1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_tip [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_impl_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_size_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_mapu [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_map [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_f_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_f_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_fu_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_fu_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_it_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_f_it_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_fu_it_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_it_impl_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_ex_it_impl_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_forget_body [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_forget_univ [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfbu_term_f_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term_f_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term_it_impl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.nth_error_All_local_env_over [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.unlift_TermTyp [in MetaRocq.Common.EnvironmentTyping]
env_prop_sigma [in MetaRocq.PCUIC.PCUICTyping]
env_prop_wf_local [in MetaRocq.PCUIC.PCUICTyping]
env_prop_typing [in MetaRocq.PCUIC.PCUICTyping]
env_prop_sigma [in MetaRocq.Template.Typing]
env_prop_wf_local [in MetaRocq.Template.Typing]
env_prop_typing [in MetaRocq.Template.Typing]
env_closed_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
env_eq [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eqb_true_iff [in MetaRocq.Common.Universes]
eqb_ctx_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_refl [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_binder_annot_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_refl [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_impl [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annots_reflect [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annots_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annot_refl [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annot_reflect [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annot_spec [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_of_listable_spec [in MetaRocq.Utils.MRListable]
eqb_of_listable_eq [in MetaRocq.Utils.MRListable]
eqb_of_listable_bl [in MetaRocq.Utils.MRListable]
eqb_of_listable_lb [in MetaRocq.Utils.MRListable]
eqb_of_listable_refl [in MetaRocq.Utils.MRListable]
eqb_annot_reflect [in MetaRocq.PCUIC.utils.PCUICAstUtils]
eqb_universe_instance_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance_spec [in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_refl [in MetaRocq.Utils.ReflectEq]
eqb_eq [in MetaRocq.Utils.ReflectEq]
eqb_specT [in MetaRocq.Utils.ReflectEq]
eqt_eqterm [in MetaRocq.SafeChecker.PCUICSafeConversion]
equal_subst_instance_cstrs_mono [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Equal_graph_edges [in MetaRocq.Common.uGraph]
equiv_env_inter_hlookup [in MetaRocq.Erasure.ErasureFunction]
equiv_env_inter_sym [in MetaRocq.Erasure.ErasureFunction]
equiv_reflect [in MetaRocq.SafeChecker.PCUICEqualityDec]
equiv_reflectT [in MetaRocq.Utils.MRReflect]
eq_term_eq_termp [in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_mkApps [in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_eq_term_napp [in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_App [in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_valid_pos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
eq_term_upto_valid_pos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
eq_context_upto_context_choice_term [in MetaRocq.PCUIC.Syntax.PCUICPosition]
eq_context_upto_names_upto_names [in MetaRocq.PCUIC.PCUICSR]
eq_ws_cumul_pb_terms_trans [in MetaRocq.PCUIC.PCUICSR]
eq_ws_cumul_pb_trans [in MetaRocq.PCUIC.PCUICSR]
eq_context_alpha_to_extended_list [in MetaRocq.PCUIC.PCUICSR]
eq_context_alpha_reln [in MetaRocq.PCUIC.PCUICSR]
eq_context_alpha_conv [in MetaRocq.PCUIC.PCUICSR]
eq_form [in MetaRocq.Examples.tauto]
eq_var [in MetaRocq.Examples.tauto]
eq_term_nl_eq [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl_IH [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_upto_names_eq_context_alpha [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_upto_names_smash_context [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_fold [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_map2_set_binder_name_eq [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_map2_set_binder_name [in MetaRocq.PCUIC.PCUICEquality]
eq_context_gen_map2_set_binder_name [in MetaRocq.PCUIC.PCUICEquality]
eq_annots_inst_case_context [in MetaRocq.PCUIC.PCUICEquality]
eq_annots_subst_instance_ctx [in MetaRocq.PCUIC.PCUICEquality]
eq_annots_lift_context [in MetaRocq.PCUIC.PCUICEquality]
eq_annots_subst_context [in MetaRocq.PCUIC.PCUICEquality]
eq_annots_fold [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_binder_annot [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_flip [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_flip [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_inv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn_inv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn_r [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICEquality]
eq_context_impl [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_nth_error [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_smash_context [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_subst_context [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_length [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_rev' [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_rev [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_cat [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_sym [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_impl [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_isApp [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_r_inv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_l_inv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_r_inv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_l_inv [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps [in MetaRocq.PCUIC.PCUICEquality]
eq_term_eq_term_napp [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_subst [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_substs [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_lift_context [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_lift [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_antisym [in MetaRocq.PCUIC.PCUICEquality]
eq_binder_relevances_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_context_gen_impl [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_gen [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_gen [in MetaRocq.PCUIC.PCUICEquality]
eq_rect_transport [in MetaRocq.Utils.MREquality]
eq_univ_prop_compare_sort_propositional_r [in MetaRocq.PCUIC.PCUICElimination]
eq_univ_prop_compare_sort_propositional [in MetaRocq.PCUIC.PCUICElimination]
eq_sort_config_impl [in MetaRocq.Common.Universes]
eq_universe_config_impl [in MetaRocq.Common.Universes]
eq_sort_subset [in MetaRocq.Common.Universes]
eq_universe_subset [in MetaRocq.Common.Universes]
eq_universe_leq_universe [in MetaRocq.Common.Universes]
eq_term_subset [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_term_upto_univ_mkApps [in MetaRocq.Template.TermEquality]
eq_term_App [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_App [in MetaRocq.Template.TermEquality]
eq_term_leq_term [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_morphism [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_morphism0 [in MetaRocq.Template.TermEquality]
eq_term_refl [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_refl [in MetaRocq.Template.TermEquality]
eq_sortP_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_universeP_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_dec_to_bool_refl [in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_context_cumul_Spec_rel [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
eq_context_cumul_Spec [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
eq_term_set_binder_name [in MetaRocq.PCUIC.PCUICValidity]
eq_binder_annots_eq_ctx [in MetaRocq.PCUIC.PCUICValidity]
eq_context_upto_univ_cumul_context [in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_univ_conv_context [in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_names_conv_context [in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_cumul_context [in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_conv_context [in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_cumul_pb_context [in MetaRocq.PCUIC.PCUICContextConversion]
eq_leq_context_upto [in MetaRocq.PCUIC.PCUICContextConversion]
eq_term_upto_univ_napp_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx_alpha [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_app [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_subst_instance [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance' [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance [in MetaRocq.PCUIC.PCUICConfluence]
eq_term_upto_univ_subst_instance' [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_univ_subst_preserved [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_eq_context_upto [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_extended_subst [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_gen_context_assumptions [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_extended_subst [in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_context_assumptions [in MetaRocq.PCUIC.PCUICConfluence]
eq_annots_expand_lets_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_instance_pcuic [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_context_pcuic [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_term_upto_univ_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_binder_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_smash_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_term_inds [in MetaRocq.PCUIC.PCUICConversion]
eq_term_compare_term [in MetaRocq.PCUIC.PCUICConversion]
eq_context_upto_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICConversion]
eq_term_fix_or_cofix [in MetaRocq.PCUIC.PCUICConversion]
eq_context_upto_names_inst_case_context [in MetaRocq.PCUIC.PCUICConversion]
eq_context_upto_names_subst_context [in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_r [in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_l [in MetaRocq.PCUIC.PCUICConversion]
eq_terms_ws_cumul_pb_terms [in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_cumulSpec [in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_napp_cumulSpec [in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_napp_0 [in MetaRocq.PCUIC.PCUICAlpha]
eq_context_conversion [in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_names_eq_context_alpha [in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_subst_instance [in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_conv_context_rel [in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_empty_impl [in MetaRocq.PCUIC.PCUICAlpha]
eq_term_upto_univ_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
eq_eta_global_env [in MetaRocq.Erasure.Typed.CertifyingEta]
eq_pair_transport [in MetaRocq.PCUIC.Syntax.PCUICViews]
eq_names_subst_instance [in MetaRocq.PCUIC.PCUICContexts]
eq_names_subst_context [in MetaRocq.PCUIC.PCUICContexts]
eq_binder_annots_eq [in MetaRocq.PCUIC.PCUICCasesContexts]
eq_names_subst_instance [in MetaRocq.PCUIC.PCUICCasesContexts]
eq_names_subst_context [in MetaRocq.PCUIC.PCUICCasesContexts]
eq_projection_refl [in MetaRocq.Common.Kernames]
eq_inductive_refl [in MetaRocq.Common.Kernames]
eq_kername_refl [in MetaRocq.Common.Kernames]
eq_term_prop_mkApps_inv [in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_eq_term_prop_impl [in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_prop_impl [in MetaRocq.PCUIC.PCUICCumulProp]
eq_tip_skipn [in MetaRocq.Template.TypingWf]
eq_decompose_app [in MetaRocq.Template.TypingWf]
eq_term_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_valuation [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_termp_mkApps_inv [in MetaRocq.PCUIC.PCUICConvCumInversion]
eq_term_upto_univ_napp_nonind [in MetaRocq.PCUIC.PCUICConvCumInversion]
eq_term_eq_termp [in MetaRocq.PCUIC.PCUICConvCumInversion]
eq_kername_eq [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eq_term_config_impl [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
eq_term_valid_pos [in MetaRocq.SafeChecker.PCUICSafeConversion]
eq_context_upto_inst_case_context [in MetaRocq.PCUIC.PCUICPrincipality]
eq_context_empty_eq_context [in MetaRocq.PCUIC.PCUICPrincipality]
eq_term_empty_eq_term [in MetaRocq.PCUIC.PCUICPrincipality]
eq_term_empty_leq_term [in MetaRocq.PCUIC.PCUICPrincipality]
eq_term_leq_term [in MetaRocq.PCUIC.PCUICPrincipality]
eq_context_gen_wf_branch [in MetaRocq.SafeChecker.PCUICTypeChecker]
eq_context_gen_wf_predicate [in MetaRocq.SafeChecker.PCUICTypeChecker]
eq_names_subst_instance_pcuic [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context_pcuic [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_binder_trans [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names_subst_instance [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_term_upto_univ_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
eq_annots_cstr_branch_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_annots_ind_predicate_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_annots_expand_lets_ctx [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_binder_annot_eq_context_gen_set_binder_name [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_prod_refl [in MetaRocq.Utils.ReflectEq]
eq0_leq0_universe [in MetaRocq.Common.Universes]
erasable_tBox_value [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_global_wf_glob [in MetaRocq.Erasure.ErasureCorrectness]
erases_mutual_inductive_body_wf [in MetaRocq.Erasure.ErasureCorrectness]
erases_global_decls_fresh [in MetaRocq.Erasure.ErasureCorrectness]
erases_global_closed_env [in MetaRocq.Erasure.ErasureCorrectness]
erases_correct [in MetaRocq.Erasure.ErasureCorrectness]
erases_lazy [in MetaRocq.Erasure.ErasureCorrectness]
erases_mutual [in MetaRocq.Erasure.ErasureFunction]
erases_weakening_env [in MetaRocq.Erasure.ErasureFunction]
erases_erase [in MetaRocq.Erasure.ErasureFunction]
erases_wellformed [in MetaRocq.Erasure.ErasureProperties]
erases_closed [in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance_decl [in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance'' [in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance [in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance0 [in MetaRocq.Erasure.ErasureProperties]
erases_context_conversion [in MetaRocq.Erasure.ErasureProperties]
erases_isLambda [in MetaRocq.Erasure.ErasureProperties]
erases_mkApps_inv [in MetaRocq.Erasure.ErasureProperties]
erases_mkApps [in MetaRocq.Erasure.ErasureProperties]
erases_App [in MetaRocq.Erasure.ErasureProperties]
erases_ext_eq [in MetaRocq.Erasure.ErasureProperties]
erases_firstorder' [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_firstorder [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_global_erase_global [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_wf_fixpoints [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_wellformed [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_erase_weaken [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_erase [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_weaken [in MetaRocq.Erasure.ErasureFunctionProperties]
erases_global_erases_deps [in MetaRocq.Erasure.EDeps]
erases_global_all_deps [in MetaRocq.Erasure.EDeps]
erases_deps_single [in MetaRocq.Erasure.EDeps]
erases_declared_constructor [in MetaRocq.Erasure.EDeps]
erases_deps_cons [in MetaRocq.Erasure.EDeps]
erases_deps_forall_ind [in MetaRocq.Erasure.EDeps]
erases_deps_eval [in MetaRocq.Erasure.EDeps]
erases_deps_cunfold_cofix [in MetaRocq.Erasure.EDeps]
erases_deps_cunfold_fix [in MetaRocq.Erasure.EDeps]
erases_deps_substl [in MetaRocq.Erasure.EDeps]
erases_deps_csubst [in MetaRocq.Erasure.EDeps]
erases_deps_subst1 [in MetaRocq.Erasure.EDeps]
erases_deps_subst [in MetaRocq.Erasure.EDeps]
erases_deps_lift [in MetaRocq.Erasure.EDeps]
erases_deps_mkApps_inv [in MetaRocq.Erasure.EDeps]
erases_deps_mkApps [in MetaRocq.Erasure.EDeps]
erases_subst0 [in MetaRocq.Erasure.ESubstitution]
erases_subst [in MetaRocq.Erasure.ESubstitution]
erases_eq [in MetaRocq.Erasure.ESubstitution]
erases_weakening [in MetaRocq.Erasure.ESubstitution]
erases_weakening' [in MetaRocq.Erasure.ESubstitution]
erases_ctx_ext [in MetaRocq.Erasure.ESubstitution]
erases_extends' [in MetaRocq.Erasure.ESubstitution]
erases_extends [in MetaRocq.Erasure.ESubstitution]
erases_wf_inductives_mapping [in MetaRocq.ErasurePlugin.Erasure]
erases_global_lookup_env_none [in MetaRocq.ErasurePlugin.Erasure]
erases_global_lookup_env_inductive [in MetaRocq.ErasurePlugin.Erasure]
erases_global_lookup_env_constant [in MetaRocq.ErasurePlugin.Erasure]
erases_forall_list_ind [in MetaRocq.Erasure.Extract]
erase_constant_body_correct' [in MetaRocq.Erasure.ErasureFunction]
erase_constant_body_correct [in MetaRocq.Erasure.ErasureFunction]
erase_global_irr [in MetaRocq.Erasure.ErasureFunction]
erase_global_deps_irr [in MetaRocq.Erasure.ErasureFunction]
erase_constant_decl_irrel [in MetaRocq.Erasure.ErasureFunction]
erase_constant_body_irrel [in MetaRocq.Erasure.ErasureFunction]
erase_irrel_global_env [in MetaRocq.Erasure.ErasureFunction]
erase_to_box [in MetaRocq.Erasure.ErasureFunction]
erase_terms_eq [in MetaRocq.Erasure.ErasureFunction]
erase_irrel [in MetaRocq.Erasure.ErasureFunction]
erase_global_decls_deps_recursive_correct [in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_global_decls_deps_recursive_correct_gen [in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_ind_correct [in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_ind_body_wellformed [in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_ind_body_correct [in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_wellformed_fast [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_fast_wf_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast_erase_global_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast_spec [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast_spec_gen [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct_strong [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct_strong' [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_eval_to_box_eager [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_eval_to_box [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_eval [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_wf_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_ind_decl_wf_glob' [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_cst_wf_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_constant_body_correct_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_wf_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_ind_decl_wf_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_cst_decl_wf_glob [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_constant_body_correct'' [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_wellformed_weaken [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_wellformed_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_wellformed [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_wf_fixpoints [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_closed [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_cofix_eq [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_fix_eq [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_brs_eq [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_fresh [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fresh [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_declared_constructor [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_erase_global [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_constant_decl_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_mkApps [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_includes [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_erases_deps [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_eta_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_function_to_function [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_function [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_transform_fo [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_transform_fo_gen [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_tranform_firstorder [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_erasable [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
erase_pcuic_program_normalization_helper [in MetaRocq.ErasurePlugin.ETransform]
erasure_pipeline_extends_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
etaExp_csubst [in MetaRocq.Erasure.EEtaExpanded]
etaExp_fixsubst [in MetaRocq.Erasure.EEtaExpandedFix]
etaExp_csubst [in MetaRocq.Erasure.EEtaExpandedFix]
etaExp_csubst' [in MetaRocq.Erasure.EEtaExpandedFix]
eta_expand_erase [in MetaRocq.Erasure.ErasureFunctionProperties]
eta_expand_global_env_expanded [in MetaRocq.Template.EtaExpand]
eta_context_assumptions [in MetaRocq.Template.EtaExpand]
eta_expand_global_decl_expanded [in MetaRocq.Template.EtaExpand]
eta_context_length [in MetaRocq.Template.EtaExpand]
eta_expand_context_sorts [in MetaRocq.Template.EtaExpand]
eta_expand_context [in MetaRocq.Template.EtaExpand]
eta_declared_constructor [in MetaRocq.Template.EtaExpand]
eta_lookup_global_error [in MetaRocq.Template.EtaExpand]
eta_lookup_global [in MetaRocq.Template.EtaExpand]
eta_expand_expanded [in MetaRocq.Template.EtaExpand]
eta_lookup_inductive_ctors [in MetaRocq.ErasurePlugin.Erasure]
eta_pair [in MetaRocq.SafeChecker.PCUICSafeConversion]
ETransformPresFO.proper_pres [in MetaRocq.ErasurePlugin.ErasureCorrectness]
eval_global_deps [in MetaRocq.Erasure.ErasureFunction]
eval_proj_eval_inv_discr [in MetaRocq.Erasure.ErasureProperties]
eval_case_eval_inv_discr [in MetaRocq.Erasure.ErasureProperties]
eval_case_eval_discr [in MetaRocq.Erasure.ErasureProperties]
eval_case_tBox_inv [in MetaRocq.Erasure.ErasureProperties]
eval_empty_brs [in MetaRocq.Erasure.ErasureProperties]
eval_preserve_mkApps_ind [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
eval_beta_inv [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
eval_mkApps_cong [in MetaRocq.Template.WcbvEval]
eval_Const [in MetaRocq.Template.WcbvEval]
eval_LetIn [in MetaRocq.Template.WcbvEval]
eval_to_stuck_fix_inv [in MetaRocq.Template.WcbvEval]
eval_atom_inj [in MetaRocq.Template.WcbvEval]
eval_to_value [in MetaRocq.Template.WcbvEval]
eval_mkApps_rect [in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_heads_deriv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_heads_deriv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_deriv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_deriv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_heads [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_tLambda_inv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tLambda_inv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tLetIn_inv [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_heads [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_args [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_head [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_arg [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_head [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_wt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eval_etaexp [in MetaRocq.Erasure.EWcbvEvalEtaInd]
eval_preserve_mkApps_ind [in MetaRocq.Erasure.EWcbvEvalEtaInd]
eval_preserve_mkApps_ind [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
eval_wf [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_cong [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_value_cong [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_value_cong [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_stuck_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_to_stuck_fix_inv [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_tApp [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_eval [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_inv [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_opt_to_target [in MetaRocq.Erasure.EEtaExpandedFix]
eval_app_cong_mkApps [in MetaRocq.Erasure.EEtaExpandedFix]
eval_value_cong [in MetaRocq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp' [in MetaRocq.Erasure.EEtaExpandedFix]
eval_stuck_fix_eq [in MetaRocq.Erasure.EEtaExpandedFix]
eval_etaexp [in MetaRocq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp [in MetaRocq.Erasure.EEtaExpandedFix]
eval_is_box [in MetaRocq.Erasure.EOptimizePropDiscr]
eval_mkApps_Construct_inv [in MetaRocq.Erasure.EConstructorsAsBlocks]
eval_tCase [in MetaRocq.PCUIC.PCUICProgress]
eval_box_apps [in MetaRocq.Erasure.EWcbvEval]
eval_construct_size [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_size [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_inv_size [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_block_inv [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_inv [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_inv' [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size_unguarded [in MetaRocq.Erasure.EWcbvEval]
eval_to_values [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size [in MetaRocq.Erasure.EWcbvEval]
eval_wellformed [in MetaRocq.Erasure.EWcbvEval]
eval_closed [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_inv [in MetaRocq.Erasure.EWcbvEval]
eval_trans [in MetaRocq.Erasure.EWcbvEval]
eval_trans' [in MetaRocq.Erasure.EWcbvEval]
eval_deterministic_all [in MetaRocq.Erasure.EWcbvEval]
eval_value [in MetaRocq.Erasure.EWcbvEval]
eval_deterministic [in MetaRocq.Erasure.EWcbvEval]
eval_unique [in MetaRocq.Erasure.EWcbvEval]
eval_unique_sig [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_cong [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tBox [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_CoFix [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_block [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct [in MetaRocq.Erasure.EWcbvEval]
eval_stuck_Fix [in MetaRocq.Erasure.EWcbvEval]
eval_to_mkApps_tBox_inv [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv [in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tCoFix [in MetaRocq.Erasure.EWcbvEval]
eval_to_value [in MetaRocq.Erasure.EWcbvEval]
eval_Construct_inv [in MetaRocq.Erasure.EWcbvEval]
eval_rect [in MetaRocq.Erasure.EWcbvEval]
eval_to_eval_named_full [in MetaRocq.Erasure.EWcbvEvalNamed]
eval_to_eval_named [in MetaRocq.Erasure.EWcbvEvalNamed]
eval_construct_All2 [in MetaRocq.Erasure.EWcbvEvalNamed]
eval_wf [in MetaRocq.Erasure.EWcbvEvalNamed]
eval_represents_value [in MetaRocq.Erasure.EWcbvEvalNamed]
eval_classification [in MetaRocq.PCUIC.PCUICClassification]
eval_whne [in MetaRocq.PCUIC.PCUICClassification]
eval_tCase [in MetaRocq.Erasure.EArities]
eval_const_construct_expanded [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_debox_env_types [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_Construct_inv' [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_dearg_reduce [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_tApp_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_tConstruct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_valid_cases [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_is_expanded_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_dearg_lambdas_inv [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_Const [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_LetIn [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_unique [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_deterministic [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_unique_sig [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_tCoFix [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_tEvar [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_tVar [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_tRel [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_closed [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_stuck_fix [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_cong [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_stuck_Fix [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_tInd [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_CoFix [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_Construct [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_to_value [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_is_box [in MetaRocq.Erasure.ECoInductiveToInductive]
existsb_map [in MetaRocq.Erasure.Typed.Utils]
exists_neg_forall [in MetaRocq.Common.uGraph]
exist_irrel_eq [in MetaRocq.Erasure.EPrimitive]
exist_irrel_eq [in MetaRocq.PCUIC.utils.PCUICPrimitive]
expanded_erases [in MetaRocq.Erasure.ErasureCorrectness]
expanded_mkApps_expanded [in MetaRocq.Erasure.EEtaExpanded]
expanded_global_env_isEtaExp_env [in MetaRocq.Erasure.EEtaExpanded]
expanded_isEtaExp [in MetaRocq.Erasure.EEtaExpanded]
expanded_isEtaExp_app_ [in MetaRocq.Erasure.EEtaExpanded]
expanded_ind [in MetaRocq.Erasure.EEtaExpanded]
expanded_erase_fast [in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_erase_global_fast [in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_erase_global [in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_erase [in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_weakening_global [in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_decl_env_irrel [in MetaRocq.Template.EtaExpand]
expanded_context_env_irrel [in MetaRocq.Template.EtaExpand]
expanded_env_irrel [in MetaRocq.Template.EtaExpand]
expanded_eta_single_tRel_app [in MetaRocq.Template.EtaExpand]
expanded_lift' [in MetaRocq.Template.EtaExpand]
expanded_lift [in MetaRocq.Template.EtaExpand]
expanded_unlift [in MetaRocq.Template.EtaExpand]
expanded_mkApps [in MetaRocq.Template.EtaExpand]
expanded_mkApps_inv [in MetaRocq.Template.EtaExpand]
expanded_tApps_inv [in MetaRocq.Template.EtaExpand]
expanded_tApp_args [in MetaRocq.Template.EtaExpand]
expanded_mkApps_tFix_inv [in MetaRocq.Template.EtaExpand]
expanded_mkApps_tFix [in MetaRocq.Template.EtaExpand]
expanded_mkApps_tConstruct [in MetaRocq.Template.EtaExpand]
expanded_fold_lambda [in MetaRocq.Template.EtaExpand]
expanded_ind [in MetaRocq.Template.EtaExpand]
expanded_expand_lets_program [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_global_env_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_smash_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_trans_local [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_tApp_arg [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_red [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_red1 [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_env_constant [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_weakening_env [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_unfold_cofix [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_unfold_fix [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_fix_subst [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps_inv' [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tPrim_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tCoFix_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tProj_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tCase_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tEvar_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tLetIn_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tLambda_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tApp_inv [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tApp [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_weakening [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_subst_instance [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_let_expansion [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_subst [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_lift [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps_expanded [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_ind [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_env_isEtaExp_env [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_isEtaExp [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_isEtaExp_app_ [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_weakening [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_closed [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_ind [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_erase_global_decls_recursive [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
expanded_erase_global_decl [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
expanded_erase [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
expanded_mkApps_expanded [in MetaRocq.Erasure.EOptimizePropDiscr]
expanded_eprogram_env_expanded_eprogram_cstrs [in MetaRocq.ErasurePlugin.ETransform]
expanded_erase_program [in MetaRocq.ErasurePlugin.ETransform]
expanded_dearg_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
expanded_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
expanded_dearg_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
expanded_trans_program [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_trans_global_env [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_trans_local [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_bcontext [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_context_weakening [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_weakening [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_inds [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_context_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_let_expansion [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_extended_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_context_map2_bias_left [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expand_lets_lift_cancel [in MetaRocq.PCUIC.PCUICSR]
expand_lets_eq_map [in MetaRocq.PCUIC.PCUICSR]
expand_lets_eq [in MetaRocq.PCUIC.PCUICSR]
expand_lets_erasure [in MetaRocq.Erasure.Prelim]
expand_lets_k_nil [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
expand_lets_subst_comm' [in MetaRocq.PCUIC.PCUICSubstitution]
expand_lets_k_ctx_subst_id' [in MetaRocq.PCUIC.PCUICSpine]
expand_lets_ctx_o_lets [in MetaRocq.PCUIC.PCUICSpine]
expand_lets_eq [in MetaRocq.Template.TermEquality]
expand_firstorder_type [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_preserves_fo [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_inst_case_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_rel_ge [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_rel_lt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_ctx_fix_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_ctx_fix_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_tCoFix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_tFix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_tRel_ass [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_fo [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_sound [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_smash_context_id [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_ctx_lift_context_cancel [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_comm [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_lift [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_set_binder_name [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_subst_comm [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_subst_comm [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_app [in MetaRocq.PCUIC.PCUICConversion]
expand_lets_k_app [in MetaRocq.PCUIC.PCUICConversion]
expand_lets_transform_env [in MetaRocq.ErasurePlugin.ErasureCorrectness]
expand_lets_eta_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
expand_lets_function [in MetaRocq.ErasurePlugin.ErasureCorrectness]
expand_lets_ctx_nil [in MetaRocq.PCUIC.PCUICContexts]
expand_lets_k_ctx_nil [in MetaRocq.PCUIC.PCUICContexts]
expand_lets_smash_context [in MetaRocq.PCUIC.PCUICContexts]
expand_lets_subst_comm [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_ctx_assumption_context [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_assumption_context [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_assumption_context [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_tRel [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_mkApps [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_mkApps [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_nil [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_vdef [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vdef [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_vass [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vass [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_ctx_app [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_0 [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_to_extended_list_k [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_subst_comm [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_ctx_tip [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_ctx_snoc [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_ctx_snoc [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_ctx_lift [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_lift [in MetaRocq.PCUIC.PCUICInductives]
expand_lets_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
expr_set_forall_map [in MetaRocq.PCUIC.PCUICCumulProp]
expr_gc_declared_declared [in MetaRocq.Common.uGraph]
extended_subst_app [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
extended_subst_set_binder_name [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extended_subst_to_extended_list_k [in MetaRocq.PCUIC.PCUICContexts]
extended_subst_lift_context [in MetaRocq.PCUIC.PCUICInductives]
extended_subst_shiftn_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn_aboveP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
extends_lookup [in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_wf_sort [in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_wf_universe [in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_global_env_equiv_env [in MetaRocq.Erasure.ErasureFunctionProperties]
extends_filter [in MetaRocq.Erasure.ErasureFunctionProperties]
extends_filter_impl [in MetaRocq.Erasure.ErasureFunctionProperties]
extends_fresh [in MetaRocq.Erasure.ErasureFunctionProperties]
extends_cons [in MetaRocq.Erasure.ErasureFunctionProperties]
extends_decls_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extends_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extends_strictly_on_decls_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extends_cons_wf [in MetaRocq.Erasure.EGenericGlobalMap]
extends_cons_inv [in MetaRocq.Erasure.EGenericGlobalMap]
extends_prefix_extends [in MetaRocq.Erasure.EExtends]
extends_wf_glob [in MetaRocq.Erasure.EExtends]
extends_eq [in MetaRocq.ErasurePlugin.ErasureCorrectness]
extends_erase_pcuic_program [in MetaRocq.ErasurePlugin.ErasureCorrectness]
extends_cons_right [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extends_trans [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extends_inductive_isprop_and_pars [in MetaRocq.Erasure.EOptimizePropDiscr]
extends_cons_wf [in MetaRocq.Erasure.EGenericMapEnv]
extends_cons_inv [in MetaRocq.Erasure.EGenericMapEnv]
extends_lookup_projection [in MetaRocq.Erasure.EGenericMapEnv]
extends_lookup_projection [in MetaRocq.Erasure.EReorderCstrs]
extends_fresh [in MetaRocq.Erasure.EWellformed]
extends_wf_global_decl [in MetaRocq.Erasure.EWellformed]
extends_wellformed [in MetaRocq.Erasure.EWellformed]
extends_is_propositional [in MetaRocq.Erasure.EWellformed]
extends_constructor_isprop_pars_decl [in MetaRocq.Erasure.EWellformed]
extends_lookup_constructor [in MetaRocq.Erasure.EWellformed]
extends_lookup_inductive [in MetaRocq.Erasure.EWellformed]
extends_lookup [in MetaRocq.Erasure.EWellformed]
extends_lookup_projection [in MetaRocq.Erasure.EInlineProjections]
extends_lookup_inductive_pars [in MetaRocq.Erasure.ERemoveParams]
extends_trans_global_decls_acc [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
extends_primitive_constant [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_cofixpoint [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_fixpoint [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_check_recursivity_kind [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_local_gen [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_lookup_inductive_kind [in MetaRocq.Erasure.ECoInductiveToInductive]
extends_inductive_isprop_and_pars [in MetaRocq.Erasure.ECoInductiveToInductive]
extract_correct_gen' [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extract_correct_gen [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extract_correct [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
ext_lift [in MetaRocq.Template.EtaExpand]
| 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) |