| 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 (definition)
aboveP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]abstract_instance [in MetaRocq.Common.Universes]
abstract_env_ext_empty [in MetaRocq.SafeChecker.PCUICSafeChecker]
abstract_env_is_consistent_empty [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_empty [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_empty_ext_rel [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_empty_ext [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_make_wf_env_ext_correct [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_make_wf_env_ext [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_sq_wf [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_cored [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_impl [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_level_mem' [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_sortb [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_ext_wf_universeb [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_check_constraints [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_sort [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_universe [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_cofixguard [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_fixguard [in MetaRocq.SafeChecker.PCUICWfEnv]
abstract_env_compare_global_instance [in MetaRocq.SafeChecker.PCUICSafeConversion]
abstract_wf_cofixpoint [in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_wf_fixpoint [in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_check_recursivity_kind [in MetaRocq.SafeChecker.PCUICTypeChecker]
abstract_env_level_mem_forallb [in MetaRocq.SafeChecker.PCUICTypeChecker]
Acc_ind' [in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_equiv [in MetaRocq.SafeChecker.PCUICSafeReduce]
Acc_intro_generator [in MetaRocq.SafeChecker.PCUICSafeReduce]
add [in MetaRocq.Examples.demo]
add [in MetaRocq.Erasure.EWcbvEvalNamed]
addnP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
add_constructor [in MetaRocq.Examples.add_constructor]
add_ctor [in MetaRocq.Examples.add_constructor]
add_global_decl [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
add_suffix [in MetaRocq.Erasure.ErasureFunctionProperties]
add_gc_constraints [in MetaRocq.Template.Checker]
add_suffix_global_env [in MetaRocq.Erasure.Typed.Certifying]
add_multiple [in MetaRocq.Erasure.EWcbvEvalNamed]
add_uctx [in MetaRocq.Common.uGraph]
add_cstrs [in MetaRocq.Common.uGraph]
add_level_edges [in MetaRocq.Common.uGraph]
add_gc_of_constraint [in MetaRocq.Common.uGraph]
add' [in MetaRocq.Examples.demo]
alli [in MetaRocq.Utils.All_Forall]
alli_size [in MetaRocq.Utils.All_Forall]
Alli_sind [in MetaRocq.Utils.All_Forall]
Alli_rec [in MetaRocq.Utils.All_Forall]
Alli_ind [in MetaRocq.Utils.All_Forall]
Alli_rect [in MetaRocq.Utils.All_Forall]
allowed_eliminations_subset [in MetaRocq.Common.Universes]
allowed_eliminations_sind [in MetaRocq.Common.Universes]
allowed_eliminations_rec [in MetaRocq.Common.Universes]
allowed_eliminations_ind [in MetaRocq.Common.Universes]
allowed_eliminations_rect [in MetaRocq.Common.Universes]
All_nth_error_spec [in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_sind [in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_rec [in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_ind [in MetaRocq.Erasure.Typed.Annotations]
All_nth_error_type_rect [in MetaRocq.Erasure.Typed.Annotations]
All_local_assum_sind [in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_rec [in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_ind [in MetaRocq.PCUIC.PCUICElimination]
All_local_assum_rect [in MetaRocq.PCUIC.PCUICElimination]
all_rels [in MetaRocq.PCUIC.PCUICSpine]
All_sigma [in MetaRocq.SafeChecker.PCUICSafeChecker]
All_over [in MetaRocq.Utils.All_Forall]
All_fold_sind [in MetaRocq.Utils.All_Forall]
All_fold_rec [in MetaRocq.Utils.All_Forall]
All_fold_ind [in MetaRocq.Utils.All_Forall]
All_fold_rect [in MetaRocq.Utils.All_Forall]
all_size [in MetaRocq.Utils.All_Forall]
All_sind [in MetaRocq.Utils.All_Forall]
All_rec [in MetaRocq.Utils.All_Forall]
All_ind [in MetaRocq.Utils.All_Forall]
All_rect [in MetaRocq.Utils.All_Forall]
all_unsafe_passes [in MetaRocq.ErasurePlugin.Erasure]
all_env_flags_blocks [in MetaRocq.Erasure.EWellformed]
all_env_flags [in MetaRocq.Erasure.EWellformed]
all_term_flags [in MetaRocq.Erasure.EWellformed]
all_primitive_flags [in MetaRocq.Erasure.EWellformed]
All_rec [in MetaRocq.Erasure.EInduction]
All2i_len_sind [in MetaRocq.Utils.All_Forall]
All2i_len_rec [in MetaRocq.Utils.All_Forall]
All2i_len_ind [in MetaRocq.Utils.All_Forall]
All2i_len_rect [in MetaRocq.Utils.All_Forall]
all2i_size [in MetaRocq.Utils.All_Forall]
All2i_sind [in MetaRocq.Utils.All_Forall]
All2i_rec [in MetaRocq.Utils.All_Forall]
All2i_ind [in MetaRocq.Utils.All_Forall]
All2i_rect [in MetaRocq.Utils.All_Forall]
All2_eval_app_spec_sind [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_rec [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_ind [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_eval_app_spec_rect [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_sq [in MetaRocq.SafeChecker.PCUICSafeChecker]
All2_fold_sind [in MetaRocq.Utils.All_Forall]
All2_fold_rec [in MetaRocq.Utils.All_Forall]
All2_fold_ind [in MetaRocq.Utils.All_Forall]
All2_fold_rect [in MetaRocq.Utils.All_Forall]
all2_size [in MetaRocq.Utils.All_Forall]
All2_map_right_inv [in MetaRocq.Utils.All_Forall]
All2_map_left_inv [in MetaRocq.Utils.All_Forall]
All2_dep_sind [in MetaRocq.Utils.All_Forall]
All2_dep_rec [in MetaRocq.Utils.All_Forall]
All2_dep_ind [in MetaRocq.Utils.All_Forall]
All2_dep_rect [in MetaRocq.Utils.All_Forall]
All2_sind [in MetaRocq.Utils.All_Forall]
All2_rec [in MetaRocq.Utils.All_Forall]
All2_ind [in MetaRocq.Utils.All_Forall]
All2_rect [in MetaRocq.Utils.All_Forall]
All2_prop2 [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop2_eq [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_prop_eq [in MetaRocq.PCUIC.PCUICParallelReduction]
All2_telescope_n_sind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_rec [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_ind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_n_rect [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_sind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_rec [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_ind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_rect [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
All2_over [in MetaRocq.Erasure.EPrimitive]
all2_size [in MetaRocq.Erasure.EPrimitive]
All2_Set_sind [in MetaRocq.Erasure.EPrimitive]
All2_Set_rec [in MetaRocq.Erasure.EPrimitive]
All2_Set_ind [in MetaRocq.Erasure.EPrimitive]
All2_Set_rect [in MetaRocq.Erasure.EPrimitive]
All3_sind [in MetaRocq.Utils.All_Forall]
All3_rec [in MetaRocq.Utils.All_Forall]
All3_ind [in MetaRocq.Utils.All_Forall]
All3_rect [in MetaRocq.Utils.All_Forall]
analyze [in MetaRocq.Erasure.Typed.Optimize]
analyze_env [in MetaRocq.Erasure.Typed.Optimize]
analyze_constant [in MetaRocq.Erasure.Typed.Optimize]
analyze_top_level [in MetaRocq.Erasure.Typed.Optimize]
analyze_state [in MetaRocq.Erasure.Typed.Optimize]
aname [in MetaRocq.Common.BasicAst]
and_assum [in MetaRocq.Utils.MRProd]
annot [in MetaRocq.Erasure.Typed.Annotations]
annotate [in MetaRocq.Erasure.EWcbvEvalNamed]
annotate_types_erase_global_decls_deps_recursive [in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_types_erase_global_decl [in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_types_erase_constant_decl [in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_types [in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_defs [in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_branches [in MetaRocq.Erasure.Typed.TypeAnnotations]
annotate_env [in MetaRocq.Erasure.EWcbvEvalNamed]
AnnotOptimizePropDiscr.annots_subst_tBox [in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box_env [in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box_decl [in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box_constant_body [in MetaRocq.Erasure.Typed.TypeAnnotations]
AnnotOptimizePropDiscr.annot_remove_match_on_box [in MetaRocq.Erasure.Typed.TypeAnnotations]
annots [in MetaRocq.Erasure.Typed.Annotations]
annot_transform_type [in MetaRocq.Erasure.Typed.Annotations]
annot_mkApps [in MetaRocq.Erasure.Typed.Annotations]
annot_subst1 [in MetaRocq.Erasure.Typed.Annotations]
annot_subst [in MetaRocq.Erasure.Typed.Annotations]
annot_lift [in MetaRocq.Erasure.Typed.Annotations]
annot_extract_template_env_within_coq_sig [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_extract_template_env_within_coq [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_extract_template_env [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_extract_pcuic_env [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_compose_transforms [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_transform [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_env [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_decl [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_cst [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_debox_env_types [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_debox_type_decl [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_aux [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_case_branches [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_single [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_branch [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_branch_aux [in MetaRocq.Erasure.Typed.TypeAnnotations]
annot_dearg_lambdas [in MetaRocq.Erasure.Typed.TypeAnnotations]
anon [in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
anonb [in MetaRocq.Examples.demo]
anonymize [in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
application_atom [in MetaRocq.PCUIC.utils.PCUICAstUtils]
appstack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_All2 [in MetaRocq.Erasure.Typed.WcbvEvalAux]
app_context [in MetaRocq.Common.BasicAst]
arguments [in MetaRocq.PCUIC.utils.PCUICAstUtils]
arities_contexts [in MetaRocq.Erasure.Typed.Erasure]
arity_ass [in MetaRocq.Erasure.Typed.Erasure]
arity_ass_context [in MetaRocq.SafeChecker.PCUICSafeReduce]
arity_ass [in MetaRocq.SafeChecker.PCUICSafeReduce]
arity_spine_sind [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_rec [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_ind [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_rect [in MetaRocq.PCUIC.PCUICSpine]
ascii_cons_pos [in MetaRocq.Utils.canonicaltries.String2pos]
assumption_context_sind [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context_ind [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
atom [in MetaRocq.Template.WcbvEval]
atom [in MetaRocq.Erasure.EWcbvEval]
atom [in MetaRocq.PCUIC.PCUICReduction]
atom [in MetaRocq.PCUIC.PCUICWcbvEval]
atomic_term [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
atomic_value_sind [in MetaRocq.Template.WcbvEval]
atomic_value_rec [in MetaRocq.Template.WcbvEval]
atomic_value_ind [in MetaRocq.Template.WcbvEval]
atomic_value_rect [in MetaRocq.Template.WcbvEval]
atomic_term [in MetaRocq.Erasure.EWcbvEvalEtaInd]
atomic_term [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
atpos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
AUContext.inter [in MetaRocq.Common.Universes]
AUContext.levels [in MetaRocq.Common.Universes]
AUContext.make [in MetaRocq.Common.Universes]
AUContext.repr [in MetaRocq.Common.Universes]
AUContext.t [in MetaRocq.Common.Universes]
Aux [in MetaRocq.SafeChecker.PCUICSafeConversion]
Aux' [in MetaRocq.SafeChecker.PCUICSafeConversion]
axiom_free [in MetaRocq.Erasure.Extract]
axiom_free_value [in MetaRocq.PCUIC.PCUICClassification]
axiom_free [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) |