| 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) |
A
A [module, in MetaRocq.Examples.add_constructor]Abort [constructor, in MetaRocq.Examples.tauto]
aboveP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
AbstractConfluence [section, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Definitions [section, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Definitions.A [variable, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond [section, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.A [variable, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.R [variable, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.S [variable, in MetaRocq.PCUIC.PCUICConfluence]
AbstractConfluence.Diamond.sc [variable, in MetaRocq.PCUIC.PCUICConfluence]
abstract_eq_wf [lemma, in MetaRocq.Erasure.Typed.Erasure]
abstract_instance [definition, in MetaRocq.Common.Universes]
abstract_env_ext_empty [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
abstract_env_lookup_correct' [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_level_mem_correct' [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_sortb_correct [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_universeb_correct [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_check_constraints_correct [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_sort_correct [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_universe_correct [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_is_consistent_empty [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_empty [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_empty_ext_rel [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_empty_ext [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_make_wf_env_ext_correct [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_make_wf_env_ext [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_sq_wf [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_cored [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_impl_abstract_env_prop [instance, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_impl_abstract_env_struct [instance, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_impl [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_primitive_constant_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_guard_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_is_consistent_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_level_mem_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_leqb_level_n_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_lookup_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_pop_decls_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_add_udecl_rel [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_add_decl_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_init_correct [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_irr [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_wf [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_exists [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_irr [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_exists [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_prop [record, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_level_mem' [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_sortb [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_universeb [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_check_constraints [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_sort [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_universe [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_cofixguard [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_fixguard [definition, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_is_consistent [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_guard [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_leqb_level_n [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_level_mem [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_primitive_constant [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_lookup [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_pop_decls [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_add_udecl [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_add_decl [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_init [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_rel [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_rel [projection, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_struct [record, in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_global_instance [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
abstract_wf_cofixpoint [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_wf_fixpoint [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_check_recursivity_kind [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_env_level_mem_forallb [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_guard_impl [record, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
abs_red_r [constructor, in MetaRocq.Template.Typing]
abs_red_l [constructor, in MetaRocq.Template.Typing]
abs_red_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
abs_red_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
Acc_ind' [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_equiv [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
acc_dlexprod_gen [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_intro_generator [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.Pimpl [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.P [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.R [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator.A [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_sidecond_generator [section, in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_no_loop [lemma, in MetaRocq.Erasure.ErasureFunction]
Acc_fun [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
acc_dlexmod [lemma, in MetaRocq.PCUIC.utils.PCUICUtils]
acc_dlexprod [lemma, in MetaRocq.PCUIC.utils.PCUICUtils]
Acc_cored_cored' [lemma, in MetaRocq.PCUIC.PCUICSN]
Acc_impl [lemma, in MetaRocq.PCUIC.PCUICSN]
Acc_no_loop [lemma, in MetaRocq.SafeChecker.PCUICWfReduction]
acyclic_no_loop_add_uctx [lemma, in MetaRocq.Common.uGraph]
acyclic_no_loop_proper [instance, in MetaRocq.Common.uGraph]
add [definition, in MetaRocq.Examples.demo]
add [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
AddLevelsCstrs [section, in MetaRocq.Common.uGraph]
addnP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_strengthen_lift [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
addnP_shiftnP_k [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
addnP_closedP [lemma, in MetaRocq.PCUIC.PCUICContextReduction]
addnP_xpredT [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
addnP_shiftnP_comm [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_orP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_shiftnP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_add [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_proper_pointwise [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
addnP0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
add_constructor [definition, in MetaRocq.Examples.add_constructor]
add_ctor [definition, in MetaRocq.Examples.add_constructor]
add_global_decl [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
add_suffix_cons [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
add_suffix [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
add_gc_constraints [definition, in MetaRocq.Template.Checker]
add_suffix_global_env [definition, in MetaRocq.Erasure.Typed.Certifying]
add_multiple_app [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
add_multiple [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
add_uctx_make_graph2 [lemma, in MetaRocq.Common.uGraph]
add_gc_of_constraint_spec [lemma, in MetaRocq.Common.uGraph]
add_uctx_subgraph [lemma, in MetaRocq.Common.uGraph]
add_uctx_make_graph [lemma, in MetaRocq.Common.uGraph]
add_level_edges_add_cstrs_comm [lemma, in MetaRocq.Common.uGraph]
add_level_edges_union [lemma, in MetaRocq.Common.uGraph]
add_cstrs_union [lemma, in MetaRocq.Common.uGraph]
add_level_edges_spec [lemma, in MetaRocq.Common.uGraph]
add_uctx [definition, in MetaRocq.Common.uGraph]
add_cstrs_proper' [instance, in MetaRocq.Common.uGraph]
add_cstrs_proper [instance, in MetaRocq.Common.uGraph]
add_cstrs_spec [lemma, in MetaRocq.Common.uGraph]
add_cstrs [definition, in MetaRocq.Common.uGraph]
add_level_edges [definition, in MetaRocq.Common.uGraph]
add_gc_of_constraint [definition, in MetaRocq.Common.uGraph]
add_constructor [library]
add' [definition, in MetaRocq.Examples.demo]
ahyp [projection, in MetaRocq.Erasure.EInduction]
AHyp [record, in MetaRocq.Erasure.EInduction]
ahyp [constructor, in MetaRocq.Erasure.EInduction]
AHyp [inductive, in MetaRocq.Erasure.EInduction]
All [inductive, in MetaRocq.Utils.All_Forall]
all [constructor, in MetaRocq.Template.TemplateMonad.Common]
All [library]
All [library]
All [library]
allbiP [lemma, in MetaRocq.Utils.All_Forall]
AllEqual [constructor, in MetaRocq.Common.Universes]
alli [section, in MetaRocq.Utils.All_Forall]
alli [definition, in MetaRocq.Utils.All_Forall]
alli [section, in MetaRocq.Utils.All_Forall]
Alli [inductive, in MetaRocq.Utils.All_Forall]
AllInP [section, in MetaRocq.Utils.MRList]
AllInP.A [variable, in MetaRocq.Utils.MRList]
AllIrrelevant [constructor, in MetaRocq.Common.Universes]
Alli_impl_le [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
Alli_map_option_out_mapi_Some_spec' [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
alli_fold_context_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
alli_subst_instance [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
Alli_helper [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
Alli_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
Alli_nth_hyp [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
Alli_nth_hyp_ind [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
alli_fold_context_k_prop [lemma, in MetaRocq.Common.BasicAst]
Alli_rev_All_fold [lemma, in MetaRocq.Utils.All_Forall]
Alli_All_fold [lemma, in MetaRocq.Utils.All_Forall]
Alli_All_fold.A [variable, in MetaRocq.Utils.All_Forall]
Alli_All_fold [section, in MetaRocq.Utils.All_Forall]
Alli_map_option_out_mapi_Some_spec [lemma, in MetaRocq.Utils.All_Forall]
Alli_map_id [lemma, in MetaRocq.Utils.All_Forall]
Alli_mapi_id [lemma, in MetaRocq.Utils.All_Forall]
Alli_mapi_spec [lemma, in MetaRocq.Utils.All_Forall]
alli_size [definition, in MetaRocq.Utils.All_Forall]
Alli_size.fn [variable, in MetaRocq.Utils.All_Forall]
Alli_size.P [variable, in MetaRocq.Utils.All_Forall]
Alli_size.A [variable, in MetaRocq.Utils.All_Forall]
Alli_size [section, in MetaRocq.Utils.All_Forall]
Alli_All_mix [lemma, in MetaRocq.Utils.All_Forall]
Alli_shiftn_inv [lemma, in MetaRocq.Utils.All_Forall]
Alli_shiftn [lemma, in MetaRocq.Utils.All_Forall]
Alli_rev_nth_error [lemma, in MetaRocq.Utils.All_Forall]
Alli_app_inv [lemma, in MetaRocq.Utils.All_Forall]
Alli_rev_inv [lemma, in MetaRocq.Utils.All_Forall]
Alli_rev [lemma, in MetaRocq.Utils.All_Forall]
Alli_refl [lemma, in MetaRocq.Utils.All_Forall]
Alli_shift [lemma, in MetaRocq.Utils.All_Forall]
Alli_mapi [lemma, in MetaRocq.Utils.All_Forall]
Alli_nth_error [lemma, in MetaRocq.Utils.All_Forall]
Alli_app [lemma, in MetaRocq.Utils.All_Forall]
Alli_All [lemma, in MetaRocq.Utils.All_Forall]
Alli_mix [lemma, in MetaRocq.Utils.All_Forall]
Alli_impl [lemma, in MetaRocq.Utils.All_Forall]
Alli_impl_Alli [lemma, in MetaRocq.Utils.All_Forall]
alli_mapi [lemma, in MetaRocq.Utils.All_Forall]
alli_map [lemma, in MetaRocq.Utils.All_Forall]
alli_shift [lemma, in MetaRocq.Utils.All_Forall]
alli_app [lemma, in MetaRocq.Utils.All_Forall]
alli_shiftn [lemma, in MetaRocq.Utils.All_Forall]
alli_Alli [lemma, in MetaRocq.Utils.All_Forall]
alli_impl [lemma, in MetaRocq.Utils.All_Forall]
alli_proper [instance, in MetaRocq.Utils.All_Forall]
alli_ext [lemma, in MetaRocq.Utils.All_Forall]
Alli_sind [definition, in MetaRocq.Utils.All_Forall]
Alli_rec [definition, in MetaRocq.Utils.All_Forall]
Alli_ind [definition, in MetaRocq.Utils.All_Forall]
Alli_rect [definition, in MetaRocq.Utils.All_Forall]
Alli_cons [constructor, in MetaRocq.Utils.All_Forall]
Alli_nil [constructor, in MetaRocq.Utils.All_Forall]
Alli_id [lemma, in MetaRocq.Template.TypingWf]
Alli_map [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Alli_All_mix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Alli_map [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Alli_map_option_out_mapi_Some_spec [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
alli.A [variable, in MetaRocq.Utils.All_Forall]
alli.A [variable, in MetaRocq.Utils.All_Forall]
alli.l [variable, in MetaRocq.Utils.All_Forall]
alli.l' [variable, in MetaRocq.Utils.All_Forall]
alli.p [variable, in MetaRocq.Utils.All_Forall]
alli.p [variable, in MetaRocq.Utils.All_Forall]
alli.q [variable, in MetaRocq.Utils.All_Forall]
allowed_eliminations_config_impl [lemma, in MetaRocq.Common.Universes]
allowed_eliminations_subset_impl [lemma, in MetaRocq.Common.Universes]
allowed_eliminations_subset [definition, in MetaRocq.Common.Universes]
allowed_eliminations_sind [definition, in MetaRocq.Common.Universes]
allowed_eliminations_rec [definition, in MetaRocq.Common.Universes]
allowed_eliminations_ind [definition, in MetaRocq.Common.Universes]
allowed_eliminations_rect [definition, in MetaRocq.Common.Universes]
allowed_eliminations [inductive, in MetaRocq.Common.Universes]
All_nth_error_spec [definition, in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_sind [definition, in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_rec [definition, in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_ind [definition, in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_rect [definition, in MetaRocq.Erasure.Typed.Annotations]
all_nth_error_None [constructor, in MetaRocq.Erasure.Typed.Annotations]
all_nth_error_Some [constructor, in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type [inductive, in MetaRocq.Erasure.Typed.Annotations]
All_local_env_Pclosed [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
All_mapi_spec [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
All_mfix_wf [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
All_local_env_inst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
All_local_env_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
All_local_assum_subst [lemma, in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_app [lemma, in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_sind [definition, in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_rec [definition, in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_ind [definition, in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_rect [definition, in MetaRocq.PCUIC.PCUICElimination]
All_local_assum [inductive, in MetaRocq.PCUIC.PCUICElimination]
all_rels_subst_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
all_rels_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
all_rels_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
all_rels_length [lemma, in MetaRocq.PCUIC.PCUICSpine]
all_rels [definition, in MetaRocq.PCUIC.PCUICSpine]
All_map_size [lemma, in MetaRocq.PCUIC.PCUICTyping]
All_All2_diag [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
all_submodules_except [constructor, in MetaRocq.Quotation.ToPCUIC.Init]
All_All2_telescopei [lemma, in MetaRocq.PCUIC.PCUICConfluence]
All_All2_telescopei_gen [lemma, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_alpha_equivalence [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_alpha_trans [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_alpha_sym [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_alpha_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_preorder [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_equivalence [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_trans [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_sym [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_decls_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
All_fold_fold_context_k_defs [lemma, in MetaRocq.Template.EtaExpand]
all_closed [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All_local_env_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_over_All [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_closed_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_map_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All_local_env_app_l [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
All_decls_alpha_pb_map [lemma, in MetaRocq.PCUIC.PCUICConversion]
All_decls_alpha_pb_impl [lemma, in MetaRocq.PCUIC.PCUICConversion]
all_eq_term_refl [instance, in MetaRocq.PCUIC.PCUICConversion]
All_fold_nth_error [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
All_fold_map_context [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
All_decls_alpha_pb_ws_decl [lemma, in MetaRocq.PCUIC.PCUICAlpha]
All_eval_etaexp [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
all_isEtaExp_closedn [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
All_sigma [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
all_submodules_except [constructor, in MetaRocq.Quotation.ToTemplate.Init]
All_reorder_list [lemma, in MetaRocq.Erasure.EReorderCstrs]
All_depth [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
All_All2_fold_swap [lemma, in MetaRocq.Utils.All_Forall]
All_All2_fold_swap_sum [lemma, in MetaRocq.Utils.All_Forall]
All_All2_swap [lemma, in MetaRocq.Utils.All_Forall]
All_All2_swap_sum [lemma, in MetaRocq.Utils.All_Forall]
All_eta3 [lemma, in MetaRocq.Utils.All_Forall]
All_Alli_swap_iff [lemma, in MetaRocq.Utils.All_Forall]
All_map_All [lemma, in MetaRocq.Utils.All_Forall]
All_remove_last [lemma, in MetaRocq.Utils.All_Forall]
All_fold_All2_fold [lemma, in MetaRocq.Utils.All_Forall]
All_fold_All2_fold_impl [lemma, in MetaRocq.Utils.All_Forall]
All_fold_prod [lemma, in MetaRocq.Utils.All_Forall]
All_fold_Alli_rev [lemma, in MetaRocq.Utils.All_Forall]
All_fold_app [lemma, in MetaRocq.Utils.All_Forall]
All_fold_impl [lemma, in MetaRocq.Utils.All_Forall]
All_fold.P [variable, in MetaRocq.Utils.All_Forall]
All_fold.A [variable, in MetaRocq.Utils.All_Forall]
All_fold [section, in MetaRocq.Utils.All_Forall]
All_fold_app_inv [lemma, in MetaRocq.Utils.All_Forall]
All_over [definition, in MetaRocq.Utils.All_Forall]
All_fold_tip [lemma, in MetaRocq.Utils.All_Forall]
All_fold_sind [definition, in MetaRocq.Utils.All_Forall]
All_fold_rec [definition, in MetaRocq.Utils.All_Forall]
All_fold_ind [definition, in MetaRocq.Utils.All_Forall]
All_fold_rect [definition, in MetaRocq.Utils.All_Forall]
All_fold_cons [constructor, in MetaRocq.Utils.All_Forall]
All_fold_nil [constructor, in MetaRocq.Utils.All_Forall]
All_fold [inductive, in MetaRocq.Utils.All_Forall]
All_forall [lemma, in MetaRocq.Utils.All_Forall]
All_In [lemma, in MetaRocq.Utils.All_Forall]
All_All2_refl [lemma, in MetaRocq.Utils.All_Forall]
All_sq [lemma, in MetaRocq.Utils.All_Forall]
All_prod [lemma, in MetaRocq.Utils.All_Forall]
All_pair [lemma, in MetaRocq.Utils.All_Forall]
All_prod_inv [lemma, in MetaRocq.Utils.All_Forall]
All_forallb_eq_forallb [lemma, in MetaRocq.Utils.All_Forall]
All_forallb_forallb_spec [lemma, in MetaRocq.Utils.All_Forall]
All_forallb_map_spec [lemma, in MetaRocq.Utils.All_Forall]
All_All2_All2_mix [lemma, in MetaRocq.Utils.All_Forall]
All_All2 [lemma, in MetaRocq.Utils.All_Forall]
All_repeat [lemma, in MetaRocq.Utils.All_Forall]
All_All_All2 [lemma, in MetaRocq.Utils.All_Forall]
All_All2_flex [lemma, in MetaRocq.Utils.All_Forall]
All_Alli [lemma, in MetaRocq.Utils.All_Forall]
All_mapi [lemma, in MetaRocq.Utils.All_Forall]
All_forallb' [lemma, in MetaRocq.Utils.All_Forall]
All_map_id' [lemma, in MetaRocq.Utils.All_Forall]
all_size [definition, in MetaRocq.Utils.All_Forall]
All_size.fn [variable, in MetaRocq.Utils.All_Forall]
All_size.P [variable, in MetaRocq.Utils.All_Forall]
All_size.A [variable, in MetaRocq.Utils.All_Forall]
All_size [section, in MetaRocq.Utils.All_Forall]
All_safe_nth [lemma, in MetaRocq.Utils.All_Forall]
All_map_id [lemma, in MetaRocq.Utils.All_Forall]
All_map_eq [lemma, in MetaRocq.Utils.All_Forall]
All_reflect_reflect_All2 [lemma, in MetaRocq.Utils.All_Forall]
All_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All_map_inv [lemma, in MetaRocq.Utils.All_Forall]
All_map [lemma, in MetaRocq.Utils.All_Forall]
All_impl [lemma, in MetaRocq.Utils.All_Forall]
All_impl_All [lemma, in MetaRocq.Utils.All_Forall]
All_rev_inv [lemma, in MetaRocq.Utils.All_Forall]
All_rev [lemma, in MetaRocq.Utils.All_Forall]
All_rev_map [lemma, in MetaRocq.Utils.All_Forall]
All_refl [lemma, in MetaRocq.Utils.All_Forall]
All_mix [lemma, in MetaRocq.Utils.All_Forall]
All_tip [lemma, in MetaRocq.Utils.All_Forall]
All_True [lemma, in MetaRocq.Utils.All_Forall]
All_app_inv [lemma, in MetaRocq.Utils.All_Forall]
All_app [lemma, in MetaRocq.Utils.All_Forall]
All_skipn [lemma, in MetaRocq.Utils.All_Forall]
All_firstn [lemma, in MetaRocq.Utils.All_Forall]
All_forallb [lemma, in MetaRocq.Utils.All_Forall]
All_Forall [lemma, in MetaRocq.Utils.All_Forall]
All_sind [definition, in MetaRocq.Utils.All_Forall]
All_rec [definition, in MetaRocq.Utils.All_Forall]
All_ind [definition, in MetaRocq.Utils.All_Forall]
All_rect [definition, in MetaRocq.Utils.All_Forall]
All_cons [constructor, in MetaRocq.Utils.All_Forall]
All_nil [constructor, in MetaRocq.Utils.All_Forall]
All_decls_on_free_vars_map_impl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All_fold_fold_context_k [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All_decls_on_free_vars_impl [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All_decls_map [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All_or_disj [lemma, in MetaRocq.PCUIC.PCUICProgress]
all_unsafe_passes [definition, in MetaRocq.ErasurePlugin.Erasure]
all_rels_smash [lemma, in MetaRocq.PCUIC.PCUICInductives]
All_decls_map_right [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_decls_on_free_vars_map_impl_inv [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_rho [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_gen_rho [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_gen [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_IH' [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All_IH [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
all_env_flags_blocks [definition, in MetaRocq.Erasure.EWellformed]
all_env_flags [definition, in MetaRocq.Erasure.EWellformed]
all_term_flags [definition, in MetaRocq.Erasure.EWellformed]
all_primitive_flags [definition, in MetaRocq.Erasure.EWellformed]
All_local_env_wf_decls [lemma, in MetaRocq.Template.TypingWf]
All_Alli [lemma, in MetaRocq.Template.TypingWf]
All_mapi [lemma, in MetaRocq.Template.TypingWf]
All_local_env_wf_decl_inv [lemma, in MetaRocq.Template.TypingWf]
All_local_env_wf_decl [lemma, in MetaRocq.Template.TypingWf]
All_local_env_over_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
All_masked [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
All_rec [definition, in MetaRocq.Erasure.EInduction]
All_rec.proj [variable, in MetaRocq.Erasure.EInduction]
All_rec.A [variable, in MetaRocq.Erasure.EInduction]
All_rec.P [variable, in MetaRocq.Erasure.EInduction]
All_rec [section, in MetaRocq.Erasure.EInduction]
All_over_All [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All_fold_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
All_All2_refl [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All_map_option_out_map_Some_spec [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All_fold_All_mix_left [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
All_fold_map [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
All_Forall [library]
All1i_Alli_mix_left [lemma, in MetaRocq.Utils.All_Forall]
All1i_map2_right [lemma, in MetaRocq.Utils.All_Forall]
All1_map2_right [lemma, in MetaRocq.Utils.All_Forall]
All1_map2_right_inv [lemma, in MetaRocq.Utils.All_Forall]
All2 [inductive, in MetaRocq.Utils.All_Forall]
All2i [inductive, in MetaRocq.Utils.All_Forall]
All2i_map [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
All2i_All2 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_sym [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_All2_mapi [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map_left_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map_right_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2i_prod [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
All2i_Alli_mix_left [lemma, in MetaRocq.Utils.All_Forall]
All2i_map2_right [lemma, in MetaRocq.Utils.All_Forall]
All2i_All2_All2 [lemma, in MetaRocq.Utils.All_Forall]
All2i_All2_All2i_All2i [lemma, in MetaRocq.Utils.All_Forall]
All2i_All2 [lemma, in MetaRocq.Utils.All_Forall]
All2i_app_inv [lemma, in MetaRocq.Utils.All_Forall]
All2i_length [lemma, in MetaRocq.Utils.All_Forall]
All2i_app_inv_r [lemma, in MetaRocq.Utils.All_Forall]
All2i_app_inv_l [lemma, in MetaRocq.Utils.All_Forall]
All2i_nth_error_r [lemma, in MetaRocq.Utils.All_Forall]
All2i_nth_error_l [lemma, in MetaRocq.Utils.All_Forall]
All2i_nth_hyp [lemma, in MetaRocq.Utils.All_Forall]
All2i_nth_impl_gen [lemma, in MetaRocq.Utils.All_Forall]
All2i_map_right [lemma, in MetaRocq.Utils.All_Forall]
All2i_map [lemma, in MetaRocq.Utils.All_Forall]
All2i_rev_ctx_inv [lemma, in MetaRocq.Utils.All_Forall]
All2i_rev_ctx_gen [lemma, in MetaRocq.Utils.All_Forall]
All2i_rev_ctx [lemma, in MetaRocq.Utils.All_Forall]
All2i_len_rev [lemma, in MetaRocq.Utils.All_Forall]
All2i_len_impl [lemma, in MetaRocq.Utils.All_Forall]
All2i_len_length [lemma, in MetaRocq.Utils.All_Forall]
All2i_len_app [lemma, in MetaRocq.Utils.All_Forall]
All2i_len_sind [definition, in MetaRocq.Utils.All_Forall]
All2i_len_rec [definition, in MetaRocq.Utils.All_Forall]
All2i_len_ind [definition, in MetaRocq.Utils.All_Forall]
All2i_len_rect [definition, in MetaRocq.Utils.All_Forall]
All2i_len_cons [constructor, in MetaRocq.Utils.All_Forall]
All2i_len_nil [constructor, in MetaRocq.Utils.All_Forall]
All2i_len [inductive, in MetaRocq.Utils.All_Forall]
All2i_len [section, in MetaRocq.Utils.All_Forall]
All2i_rev [lemma, in MetaRocq.Utils.All_Forall]
All2i_trivial [lemma, in MetaRocq.Utils.All_Forall]
All2i_mapi_rec [lemma, in MetaRocq.Utils.All_Forall]
All2i_app [lemma, in MetaRocq.Utils.All_Forall]
All2i_mapi [lemma, in MetaRocq.Utils.All_Forall]
All2i_impl [lemma, in MetaRocq.Utils.All_Forall]
all2i_size [definition, in MetaRocq.Utils.All_Forall]
All2i_size.fn [variable, in MetaRocq.Utils.All_Forall]
All2i_size.P [variable, in MetaRocq.Utils.All_Forall]
All2i_size.B [variable, in MetaRocq.Utils.All_Forall]
All2i_size.A [variable, in MetaRocq.Utils.All_Forall]
All2i_size [section, in MetaRocq.Utils.All_Forall]
All2i_All_right [lemma, in MetaRocq.Utils.All_Forall]
All2i_All_left [lemma, in MetaRocq.Utils.All_Forall]
All2i_All2_mix_left [lemma, in MetaRocq.Utils.All_Forall]
All2i_All_mix_right [lemma, in MetaRocq.Utils.All_Forall]
All2i_All_mix_left [lemma, in MetaRocq.Utils.All_Forall]
All2i_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All2i_All2i_mix [lemma, in MetaRocq.Utils.All_Forall]
All2i_sind [definition, in MetaRocq.Utils.All_Forall]
All2i_rec [definition, in MetaRocq.Utils.All_Forall]
All2i_ind [definition, in MetaRocq.Utils.All_Forall]
All2i_rect [definition, in MetaRocq.Utils.All_Forall]
All2i_cons [constructor, in MetaRocq.Utils.All_Forall]
All2i_nil [constructor, in MetaRocq.Utils.All_Forall]
All2i_All2 [lemma, in MetaRocq.Template.TypingWf]
All2i_sym [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2i_All2_mapi [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2P [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_nth_ass [lemma, in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
All2_eq_context_upto [lemma, in MetaRocq.PCUIC.PCUICEquality]
All2_eq_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
All2_fold_len [instance, in MetaRocq.PCUIC.PCUICEquality]
All2_ctx_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
All2_fold_mapi_right [lemma, in MetaRocq.PCUIC.PCUICSpine]
All2_many_OnOne2 [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
All2_nil_rev [lemma, in MetaRocq.Template.WcbvEval]
All2_nil [lemma, in MetaRocq.Template.WcbvEval]
All2_cumul_over_refl [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
All2_conv_over_refl [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
All2_eq_binder_subst_context_inst [lemma, in MetaRocq.PCUIC.PCUICValidity]
All2_fold_red_refl [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
All2_fold_over_red_refl [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
All2_All2_fold_fix_context [lemma, in MetaRocq.PCUIC.PCUICConfluence]
All2_fold_refl [lemma, in MetaRocq.PCUIC.PCUICConfluence]
All2_eval_snoc_elim [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_sind [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_rec [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_ind [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_rect [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_intro [constructor, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec [inductive, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_rev_rect [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_split_eq [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_map_option_out_mapi_Some_spec [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2_eq_binder_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2_eq_binder_lift_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
All2_sym [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
All2_fold_context_k [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
All2_fold_inst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
All2_fold_over_same_app [lemma, in MetaRocq.PCUIC.PCUICConversion]
All2_fold_over_same [lemma, in MetaRocq.PCUIC.PCUICConversion]
All2_fold_fold_context_k [lemma, in MetaRocq.PCUIC.PCUICConversion]
All2_many_OnOne2_pres [lemma, in MetaRocq.PCUIC.PCUICConversion]
All2_fold_All_right [lemma, in MetaRocq.PCUIC.PCUICAlpha]
All2_fold_All_fold_mix_right [lemma, in MetaRocq.PCUIC.PCUICAlpha]
All2_fold_cst_map [lemma, in MetaRocq.Common.BasicAst]
All2_fold_map [lemma, in MetaRocq.Common.BasicAst]
All2_fold_mapi [lemma, in MetaRocq.Common.BasicAst]
All2_fold_impl_onctx [lemma, in MetaRocq.Common.BasicAst]
All2_eq_binder_subst_instance [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
All2_eq_binder_subst_context [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
All2_sq [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
All2_map2_right_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_map2_right [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_swap [lemma, in MetaRocq.Utils.All_Forall]
All2_All_swap [lemma, in MetaRocq.Utils.All_Forall]
All2_map2_left_All3 [lemma, in MetaRocq.Utils.All_Forall]
All2_map2_left [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_prod_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_prod [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_nth_r [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_nth [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_forallb2 [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_impl_len [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_impl_ind [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_app_inv_l [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_app_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_flip [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_sym [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_trans [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_refl [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All2 [lemma, in MetaRocq.Utils.All_Forall]
All2_fold.P [variable, in MetaRocq.Utils.All_Forall]
All2_fold.A [variable, in MetaRocq.Utils.All_Forall]
All2_fold [section, in MetaRocq.Utils.All_Forall]
All2_fold_All_left [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_right [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_left_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_right [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_All_fold_mix_left [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_impl [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_length [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_app [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_from_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All2_fold_sind [definition, in MetaRocq.Utils.All_Forall]
All2_fold_rec [definition, in MetaRocq.Utils.All_Forall]
All2_fold_ind [definition, in MetaRocq.Utils.All_Forall]
All2_fold_rect [definition, in MetaRocq.Utils.All_Forall]
All2_fold_cons [constructor, in MetaRocq.Utils.All_Forall]
All2_fold_nil [constructor, in MetaRocq.Utils.All_Forall]
All2_fold [inductive, in MetaRocq.Utils.All_Forall]
All2_In_right [lemma, in MetaRocq.Utils.All_Forall]
All2_In [lemma, in MetaRocq.Utils.All_Forall]
All2_app_r [lemma, in MetaRocq.Utils.All_Forall]
All2_sq [lemma, in MetaRocq.Utils.All_Forall]
All2_eq [lemma, in MetaRocq.Utils.All_Forall]
All2_nth_error_Some_right [lemma, in MetaRocq.Utils.All_Forall]
All2_symP [lemma, in MetaRocq.Utils.All_Forall]
All2_sym [lemma, in MetaRocq.Utils.All_Forall]
All2_prod_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_prod [lemma, in MetaRocq.Utils.All_Forall]
All2_same [lemma, in MetaRocq.Utils.All_Forall]
All2_nth_error_Some_r [lemma, in MetaRocq.Utils.All_Forall]
All2_nth_error_Some [lemma, in MetaRocq.Utils.All_Forall]
All2_impl' [lemma, in MetaRocq.Utils.All_Forall]
All2_firstn [lemma, in MetaRocq.Utils.All_Forall]
All2_swap [lemma, in MetaRocq.Utils.All_Forall]
All2_dep_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All2_dep_from_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All2_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All2_from_nth_error [lemma, in MetaRocq.Utils.All_Forall]
All2_right_triv [lemma, in MetaRocq.Utils.All_Forall]
All2_skipn [lemma, in MetaRocq.Utils.All_Forall]
All2_mapi [lemma, in MetaRocq.Utils.All_Forall]
All2_nth [lemma, in MetaRocq.Utils.All_Forall]
All2_trans' [lemma, in MetaRocq.Utils.All_Forall]
All2_trans [lemma, in MetaRocq.Utils.All_Forall]
All2_All [lemma, in MetaRocq.Utils.All_Forall]
All2_impl_In [lemma, in MetaRocq.Utils.All_Forall]
All2_rev [lemma, in MetaRocq.Utils.All_Forall]
All2_app [lemma, in MetaRocq.Utils.All_Forall]
All2_ind_rev [lemma, in MetaRocq.Utils.All_Forall]
All2_rect_rev [lemma, in MetaRocq.Utils.All_Forall]
All2_app_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_app_inv_r [lemma, in MetaRocq.Utils.All_Forall]
All2_app_inv_l [lemma, in MetaRocq.Utils.All_Forall]
All2_nth_error_None [lemma, in MetaRocq.Utils.All_Forall]
All2_length [lemma, in MetaRocq.Utils.All_Forall]
All2_All_left_pack [lemma, in MetaRocq.Utils.All_Forall]
All2_non_nil [lemma, in MetaRocq.Utils.All_Forall]
all2_size [definition, in MetaRocq.Utils.All_Forall]
All2_size.fn [variable, in MetaRocq.Utils.All_Forall]
All2_size.P [variable, in MetaRocq.Utils.All_Forall]
All2_size.B [variable, in MetaRocq.Utils.All_Forall]
All2_size.A [variable, in MetaRocq.Utils.All_Forall]
All2_size [section, in MetaRocq.Utils.All_Forall]
All2_reflect_reflect_All2 [lemma, in MetaRocq.Utils.All_Forall]
All2_mix_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_mix [lemma, in MetaRocq.Utils.All_Forall]
All2_All2_mix [lemma, in MetaRocq.Utils.All_Forall]
All2_undep [lemma, in MetaRocq.Utils.All_Forall]
All2_map_right_inv [definition, in MetaRocq.Utils.All_Forall]
All2_map_left_inv [definition, in MetaRocq.Utils.All_Forall]
All2_map_right [lemma, in MetaRocq.Utils.All_Forall]
All2_map_left' [lemma, in MetaRocq.Utils.All_Forall]
All2_map_left [lemma, in MetaRocq.Utils.All_Forall]
All2_map_right_equiv [lemma, in MetaRocq.Utils.All_Forall]
All2_map_left_equiv [lemma, in MetaRocq.Utils.All_Forall]
All2_Forall2 [lemma, in MetaRocq.Utils.All_Forall]
All2_dep_impl [lemma, in MetaRocq.Utils.All_Forall]
All2_apply_dep_All [lemma, in MetaRocq.Utils.All_Forall]
All2_apply_dep_arrow [lemma, in MetaRocq.Utils.All_Forall]
All2_apply_arrow [lemma, in MetaRocq.Utils.All_Forall]
All2_apply [lemma, in MetaRocq.Utils.All_Forall]
All2_transitivity [lemma, in MetaRocq.Utils.All_Forall]
All2_symmetry [lemma, in MetaRocq.Utils.All_Forall]
All2_reflexivity [lemma, in MetaRocq.Utils.All_Forall]
All2_eq_eq [lemma, in MetaRocq.Utils.All_Forall]
All2_impl [lemma, in MetaRocq.Utils.All_Forall]
All2_impl_All2 [lemma, in MetaRocq.Utils.All_Forall]
All2_right [lemma, in MetaRocq.Utils.All_Forall]
All2_All_right [lemma, in MetaRocq.Utils.All_Forall]
All2_All_left [lemma, in MetaRocq.Utils.All_Forall]
All2_All2_All2 [lemma, in MetaRocq.Utils.All_Forall]
All2_All_mix_right [lemma, in MetaRocq.Utils.All_Forall]
All2_All_mix_left [lemma, in MetaRocq.Utils.All_Forall]
All2_tip_l [lemma, in MetaRocq.Utils.All_Forall]
All2_map_inv [lemma, in MetaRocq.Utils.All_Forall]
All2_map [lemma, in MetaRocq.Utils.All_Forall]
All2_map_equiv [lemma, in MetaRocq.Utils.All_Forall]
All2_refl [lemma, in MetaRocq.Utils.All_Forall]
All2_forallb2 [lemma, in MetaRocq.Utils.All_Forall]
All2_dep_sind [definition, in MetaRocq.Utils.All_Forall]
All2_dep_rec [definition, in MetaRocq.Utils.All_Forall]
All2_dep_ind [definition, in MetaRocq.Utils.All_Forall]
All2_dep_rect [definition, in MetaRocq.Utils.All_Forall]
All2_dep_cons [constructor, in MetaRocq.Utils.All_Forall]
All2_dep_nil [constructor, in MetaRocq.Utils.All_Forall]
All2_dep [inductive, in MetaRocq.Utils.All_Forall]
All2_tip [lemma, in MetaRocq.Utils.All_Forall]
All2_sind [definition, in MetaRocq.Utils.All_Forall]
All2_rec [definition, in MetaRocq.Utils.All_Forall]
All2_ind [definition, in MetaRocq.Utils.All_Forall]
All2_rect [definition, in MetaRocq.Utils.All_Forall]
All2_cons [constructor, in MetaRocq.Utils.All_Forall]
All2_nil [constructor, in MetaRocq.Utils.All_Forall]
All2_fold [section, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_All2_prop2_eq [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop2 [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop2_eq [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_All2_prop_eq [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_branch_prop [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_All2_prop [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop_eq [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
All2_over_impl [lemma, in MetaRocq.Erasure.EWcbvEval]
All2_ind_OnOne2 [lemma, in MetaRocq.PCUIC.PCUICReduction]
All2_eq [lemma, in MetaRocq.PCUIC.PCUICReduction]
All2_fold_fold_context_right [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_fold_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_mapi [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_sind [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_rec [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_ind [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_rect [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n [inductive, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_sind [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_rec [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_ind [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_rect [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope [inductive, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_prop2_eq_split [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_masked [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
All2_map_option_out_mapi_Some_spec [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_eq_binder_expand_lets_ctx [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_eq_binder_lift_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_compare_decls_trans [instance, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_compare_decls_sym [instance, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_compare_decls_refl [instance, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
All2_refl_inv [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_All_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_nth_hyp [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_All2_All2_All3 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_map_option_out_mapi_Some_spec [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
All2_over_undep [lemma, in MetaRocq.Erasure.EPrimitive]
All2_over [definition, in MetaRocq.Erasure.EPrimitive]
All2_All2_Set [lemma, in MetaRocq.Erasure.EPrimitive]
All2_Set_All2 [lemma, in MetaRocq.Erasure.EPrimitive]
all2_size [definition, in MetaRocq.Erasure.EPrimitive]
All2_size.fn [variable, in MetaRocq.Erasure.EPrimitive]
All2_size.P [variable, in MetaRocq.Erasure.EPrimitive]
All2_size.B [variable, in MetaRocq.Erasure.EPrimitive]
All2_size.A [variable, in MetaRocq.Erasure.EPrimitive]
All2_size [section, in MetaRocq.Erasure.EPrimitive]
All2_Set_sind [definition, in MetaRocq.Erasure.EPrimitive]
All2_Set_rec [definition, in MetaRocq.Erasure.EPrimitive]
All2_Set_ind [definition, in MetaRocq.Erasure.EPrimitive]
All2_Set_rect [definition, in MetaRocq.Erasure.EPrimitive]
All2_cons [constructor, in MetaRocq.Erasure.EPrimitive]
All2_nil [constructor, in MetaRocq.Erasure.EPrimitive]
All2_Set [inductive, in MetaRocq.Erasure.EPrimitive]
All3 [inductive, in MetaRocq.Utils.All_Forall]
All3P [lemma, in MetaRocq.Utils.All_Forall]
All3_impl [lemma, in MetaRocq.PCUIC.PCUICNormal]
All3_impl [lemma, in MetaRocq.Utils.All_Forall]
All3_map_all [lemma, in MetaRocq.Utils.All_Forall]
All3_Forall3 [lemma, in MetaRocq.Utils.All_Forall]
All3_forallb3 [lemma, in MetaRocq.Utils.All_Forall]
All3_sind [definition, in MetaRocq.Utils.All_Forall]
All3_rec [definition, in MetaRocq.Utils.All_Forall]
All3_ind [definition, in MetaRocq.Utils.All_Forall]
All3_rect [definition, in MetaRocq.Utils.All_Forall]
All3_cons [constructor, in MetaRocq.Utils.All_Forall]
All3_nil [constructor, in MetaRocq.Utils.All_Forall]
All3_many_OnOne2All [lemma, in MetaRocq.PCUIC.PCUICReduction]
All3_length [lemma, in MetaRocq.PCUIC.PCUICReduction]
Alpha [section, in MetaRocq.PCUIC.PCUICSN]
Alpha [section, in MetaRocq.PCUIC.PCUICAlpha]
alpha_eq_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
alpha_eq_symmmetric [instance, in MetaRocq.PCUIC.PCUICEquality]
alpha_eq_reflexive [instance, in MetaRocq.PCUIC.PCUICEquality]
alpha_eq [abbreviation, in MetaRocq.Erasure.ErasureFunction]
alpha_eq_subst_context [lemma, in MetaRocq.Template.TermEquality]
alpha_eq_extended_subst [lemma, in MetaRocq.Template.TermEquality]
alpha_eq_context_assumptions [lemma, in MetaRocq.Template.TermEquality]
alpha_eq_context_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
alpha_eq_context_closed [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
alpha_eq [abbreviation, in MetaRocq.Erasure.ErasureFunctionProperties]
alpha_eq_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
alpha_eq_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
alpha_eq_subst_context [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_lift_context [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_smash_context [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_extended_subst [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_subst_instance [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
alpha_eq_trans [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
alpha_eq_on_free_vars [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
Alpha.cf [variable, in MetaRocq.PCUIC.PCUICSN]
Alpha.cf [variable, in MetaRocq.PCUIC.PCUICAlpha]
Alpha.no [variable, in MetaRocq.PCUIC.PCUICSN]
Alpha.normalization [variable, in MetaRocq.PCUIC.PCUICSN]
Alpha.Σ [variable, in MetaRocq.PCUIC.PCUICSN]
AlreadyDeclared [constructor, in MetaRocq.SafeChecker.PCUICErrors]
AlreadyDeclared [constructor, in MetaRocq.Template.Checker]
alt_into_ws_cumul_pb_terms [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
alt_conv_term [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
analyze [definition, in MetaRocq.Erasure.Typed.Optimize]
AnalyzeTop [section, in MetaRocq.Erasure.Typed.Optimize]
AnalyzeTop.analyze [variable, in MetaRocq.Erasure.Typed.Optimize]
analyze_env [definition, in MetaRocq.Erasure.Typed.Optimize]
analyze_constant [definition, in MetaRocq.Erasure.Typed.Optimize]
analyze_top_level [definition, in MetaRocq.Erasure.Typed.Optimize]
analyze_state [definition, in MetaRocq.Erasure.Typed.Optimize]
aname [definition, in MetaRocq.Common.BasicAst]
And [constructor, in MetaRocq.Examples.tauto]
andb_andI [lemma, in MetaRocq.Utils.MRProd]
andb_and [lemma, in MetaRocq.Utils.MRProd]
andb_is_true [lemma, in MetaRocq.Common.uGraph]
andP_Proper [instance, in MetaRocq.Utils.MRPred]
andP_Proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
and_assum [definition, in MetaRocq.Utils.MRProd]
and10 [inductive, in MetaRocq.Utils.MRProd]
and3 [inductive, in MetaRocq.Utils.MRProd]
and4 [inductive, in MetaRocq.Utils.MRProd]
and5 [inductive, in MetaRocq.Utils.MRProd]
and6 [inductive, in MetaRocq.Utils.MRProd]
and7 [inductive, in MetaRocq.Utils.MRProd]
and8 [inductive, in MetaRocq.Utils.MRProd]
and9 [inductive, in MetaRocq.Utils.MRProd]
annot [definition, in MetaRocq.Erasure.Typed.Annotations]
annotate [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
annotate_types_erase_global_decls_deps_recursive [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_types_erase_global_decl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_types_erase_constant_decl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_types [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_defs [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_branches [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_env [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
Annotations [library]
AnnotOptimizePropDiscr [module, in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annots_subst_tBox [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box_env [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box_decl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box_constant_body [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annots [definition, in MetaRocq.Erasure.Typed.Annotations]
annots [section, in MetaRocq.Erasure.Typed.Annotations]
annots.A [variable, in MetaRocq.Erasure.Typed.Annotations]
annots.lam_body_annot_cont.f [variable, in MetaRocq.Erasure.Typed.Annotations]
annots.lam_body_annot_cont.B [variable, in MetaRocq.Erasure.Typed.Annotations]
annots.lam_body_annot_cont [section, in MetaRocq.Erasure.Typed.Annotations]
annot_transform_type [definition, in MetaRocq.Erasure.Typed.Annotations]
annot_mkApps [definition, in MetaRocq.Erasure.Typed.Annotations]
annot_subst1 [definition, in MetaRocq.Erasure.Typed.Annotations]
annot_subst [definition, in MetaRocq.Erasure.Typed.Annotations]
annot_lift [definition, in MetaRocq.Erasure.Typed.Annotations]
annot_extract_template_env_within_coq_sig [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_extract_template_env_within_coq [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_extract_template_env [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_extract_pcuic_env [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_compose_transforms [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_transform [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_env [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_decl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_cst [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_debox_env_types [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_debox_type_decl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_aux [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_case_branches [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_single [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_branch [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_branch_aux [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_lambdas [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
anon [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
anonb [definition, in MetaRocq.Examples.demo]
anonymize [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
anonymize_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
anqme_eqdec [instance, in MetaRocq.Common.BasicAst]
app [constructor, in MetaRocq.Examples.add_constructor]
append_Empty_r [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
append_inv [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
application_atom_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
application_atom [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
apply_expanded [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
apply_expanded [lemma, in MetaRocq.Template.EtaExpand]
appstack [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
App_r [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
App_l [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_r [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_l [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_tip_nil [lemma, in MetaRocq.Utils.MRList]
app_inj_length_l [lemma, in MetaRocq.Utils.MRList]
app_inj_length_r [lemma, in MetaRocq.Utils.MRList]
app_tip_assoc [lemma, in MetaRocq.Utils.MRList]
app_cored_r [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
app_All2 [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
app_mkApps [lemma, in MetaRocq.PCUIC.PCUICConversion]
app_context_length [lemma, in MetaRocq.Common.BasicAst]
app_context_push [lemma, in MetaRocq.Common.BasicAst]
app_context_cons [lemma, in MetaRocq.Common.BasicAst]
app_context_assoc [lemma, in MetaRocq.Common.BasicAst]
app_context_nil_l [lemma, in MetaRocq.Common.BasicAst]
app_context [definition, in MetaRocq.Common.BasicAst]
app_Forall [lemma, in MetaRocq.Utils.All_Forall]
app_red_r [constructor, in MetaRocq.Template.Typing]
app_red_l [constructor, in MetaRocq.Template.Typing]
app_red_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
app_red_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
app_inj [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Args [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
arguments [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
arguments_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
arguments_mkApps_nApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
Arities [section, in MetaRocq.PCUIC.PCUICClassification]
AritiesToGeneration_typing_spine [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
arities_contexts_1 [lemma, in MetaRocq.Erasure.Typed.Erasure]
arities_contexts_cons_1 [lemma, in MetaRocq.Erasure.Typed.Erasure]
arities_contexts [definition, in MetaRocq.Erasure.Typed.Erasure]
Arities.cf [variable, in MetaRocq.PCUIC.PCUICClassification]
Arities.wfΣ [variable, in MetaRocq.PCUIC.PCUICClassification]
Arities.Σ [variable, in MetaRocq.PCUIC.PCUICClassification]
arity_ass [definition, in MetaRocq.Erasure.Typed.Erasure]
arity_ass_context [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
arity_ass [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
arity_spine_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_eq [lemma, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_it_mkProd_or_LetIn_Sort [lemma, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSpine]
arity_typing_spine [lemma, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_sind [definition, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_rec [definition, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_ind [definition, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_rect [definition, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_ass [constructor, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_def [constructor, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_conv [constructor, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_nil [constructor, in MetaRocq.PCUIC.PCUICSpine]
arity_spine [inductive, in MetaRocq.PCUIC.PCUICSpine]
arity_spine_to_extended_list_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
arity_spine_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
arity_spine_eq [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
arity_red_to_prod_or_sort [lemma, in MetaRocq.PCUIC.PCUICConversion]
arity_spine_case_predicate [lemma, in MetaRocq.PCUIC.PCUICInductives]
arity_type_inv [lemma, in MetaRocq.Erasure.EArities]
ArrayNotConvertibleDefault [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ArrayNotConvertibleLevels [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ArrayNotConvertibleTypes [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ArrayNotConvertibleValues [constructor, in MetaRocq.SafeChecker.PCUICErrors]
ArrayValuesNotSameLength [constructor, in MetaRocq.SafeChecker.PCUICErrors]
array_val [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
array_ty [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
array_def [constructor, in MetaRocq.PCUIC.Syntax.PCUICPosition]
array_red_type [constructor, in MetaRocq.Template.Typing]
array_red_def [constructor, in MetaRocq.Template.Typing]
array_red_val [constructor, in MetaRocq.Template.Typing]
array_red_type [constructor, in MetaRocq.PCUIC.PCUICReduction]
array_red_def [constructor, in MetaRocq.PCUIC.PCUICReduction]
array_red_val [constructor, in MetaRocq.PCUIC.PCUICReduction]
array_model_eqdec [instance, in MetaRocq.Erasure.EPrimitive]
array_value [projection, in MetaRocq.Erasure.EPrimitive]
array_default [projection, in MetaRocq.Erasure.EPrimitive]
array_model [record, in MetaRocq.Erasure.EPrimitive]
array_model_eqdec [instance, in MetaRocq.PCUIC.utils.PCUICPrimitive]
array_value [projection, in MetaRocq.PCUIC.utils.PCUICPrimitive]
array_default [projection, in MetaRocq.PCUIC.utils.PCUICPrimitive]
array_type [projection, in MetaRocq.PCUIC.utils.PCUICPrimitive]
array_level [projection, in MetaRocq.PCUIC.utils.PCUICPrimitive]
array_model [record, in MetaRocq.PCUIC.utils.PCUICPrimitive]
ascii_cons_pos [definition, in MetaRocq.Utils.canonicaltries.String2pos]
ascii_eqdec [instance, in MetaRocq.Utils.MRPrelude]
assume_env_wellformed [axiom, in MetaRocq.Erasure.Typed.Extraction]
assume_normalization [instance, in MetaRocq.Examples.typing_correctness]
assume_wt_template_program [axiom, in MetaRocq.Template.TemplateCheckWf]
assume_that_we_only_erase_on_welltyped_programs [axiom, in MetaRocq.ErasurePlugin.Erasure]
assume_that_we_only_erase_on_wellformed_inductive_mappings [axiom, in MetaRocq.ErasurePlugin.Erasure]
assume_preservation_template_program_env_expansion [axiom, in MetaRocq.ErasurePlugin.Erasure]
assume_welltyped_template_program_expansion [axiom, in MetaRocq.ErasurePlugin.Erasure]
assume_normalization [instance, in MetaRocq.Examples.metarocq_tour_prelude]
assumption_context_compare_decls [lemma, in MetaRocq.Erasure.Prelim]
assumption_context_cstr_branch_context [lemma, in MetaRocq.Erasure.Prelim]
assumption_context_map2_binders [lemma, in MetaRocq.Erasure.Prelim]
assumption_context_sind [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context_ind [definition, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context_vass [constructor, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context_nil [constructor, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context [inductive, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context_arity_ass_context [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
assumption_context_skipn [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
assumption_context_app_inv [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
assumption_context_arities_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
assumption_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
assumption_context_lift_context [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_subst_context [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_subst_instance [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_map [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
assumption_context_fold [lemma, in MetaRocq.PCUIC.PCUICContexts]
assumption_context_length [lemma, in MetaRocq.PCUIC.PCUICContexts]
assumption_context_app [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
assumption_context_firstn [lemma, in MetaRocq.PCUIC.PCUICClassification]
assumption_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICClassification]
assumption_context_rev [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
assumption_context_subst_telescope [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
Ast [library]
AstUtils [library]
Ast_inst_case_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Ast_inst_case_context_length [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Ast_cstr_branch_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
atom [definition, in MetaRocq.Template.WcbvEval]
atom [definition, in MetaRocq.Erasure.EWcbvEval]
atom [definition, in MetaRocq.PCUIC.PCUICReduction]
atom [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
atomic [abbreviation, in MetaRocq.Template.WcbvEval]
atomic [abbreviation, in MetaRocq.Erasure.EWcbvEval]
atomic_term [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
atomic_value_sind [definition, in MetaRocq.Template.WcbvEval]
atomic_value_rec [definition, in MetaRocq.Template.WcbvEval]
atomic_value_ind [definition, in MetaRocq.Template.WcbvEval]
atomic_value_rect [definition, in MetaRocq.Template.WcbvEval]
atomic_array [constructor, in MetaRocq.Template.WcbvEval]
atomic_atom [constructor, in MetaRocq.Template.WcbvEval]
atomic_value [inductive, in MetaRocq.Template.WcbvEval]
atomic_term [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
atomic_term [definition, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
atomic_primitive [constructor, in MetaRocq.Erasure.EWcbvEval]
atomic_atom [constructor, in MetaRocq.Erasure.EWcbvEval]
atomic_value [inductive, in MetaRocq.Erasure.EWcbvEval]
atomic_primitive [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
atomic_atom [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
atomic_value [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
atom_decompose_app [lemma, in MetaRocq.Template.AstUtils]
atom_nApp [lemma, in MetaRocq.Template.WcbvEval]
atom_mkApps [lemma, in MetaRocq.Template.WcbvEval]
atom_decompose_app [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
atom_nApp [lemma, in MetaRocq.Erasure.EWcbvEval]
atom_mkApps [lemma, in MetaRocq.Erasure.EWcbvEval]
atom_mkApps [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
atom_nApp [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
atom_mkApps [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
atpos [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
atpos_assoc [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
AUContext [module, in MetaRocq.Common.Universes]
AUContext.inter [definition, in MetaRocq.Common.Universes]
AUContext.levels [definition, in MetaRocq.Common.Universes]
AUContext.make [definition, in MetaRocq.Common.Universes]
AUContext.repr [definition, in MetaRocq.Common.Universes]
AUContext.t [definition, in MetaRocq.Common.Universes]
Aux [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
Aux' [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
axiom_free [definition, in MetaRocq.Erasure.Extract]
axiom_free_value_mkApps [lemma, in MetaRocq.PCUIC.PCUICClassification]
axiom_free_axiom_free_value [lemma, in MetaRocq.PCUIC.PCUICClassification]
axiom_free_value [definition, in MetaRocq.PCUIC.PCUICClassification]
axiom_free [definition, in MetaRocq.PCUIC.PCUICClassification]
| 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) |