| 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) |
T (lemma)
tApp_mkApps [in MetaRocq.Erasure.EImplementBox]tApp_mkApps [in MetaRocq.SafeChecker.PCUICSafeReduce]
tApp_mkApps_inj [in MetaRocq.PCUIC.utils.PCUICAstUtils]
tApp_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
tApp_mkApps [in MetaRocq.Erasure.EConstructorsAsBlocks]
target_edge_of_level [in MetaRocq.Common.uGraph]
tauto_sound [in MetaRocq.Examples.tauto]
tCoFix_no_Type [in MetaRocq.Erasure.EArities]
tConstruct_no_Type [in MetaRocq.Erasure.EArities]
template_to_pcuic_typing [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_to_pcuic_env_ext [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_to_pcuic_env [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_to_pcuic [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_wf_cons_inv [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
TermSpineView.view_mkApps [in MetaRocq.Erasure.ESpineView]
terms_global_deps_skipn [in MetaRocq.Erasure.ErasureFunction]
terms_global_deps_rev [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_cunfold_cofix [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_cofix_subst [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_cunfold_fix [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_fix_subst [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_repeat [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_iota_red [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_substl [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_mkApps [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_fresh [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_csubst [in MetaRocq.Erasure.ErasureFunction]
term_global_deps_spec [in MetaRocq.Erasure.ErasureFunctionProperties]
term_wf_forall_list_ind [in MetaRocq.Template.WfAst]
term_ind_size_app [in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_forall_ctx_list_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_forall_mkApps_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_forall_list_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_ind_depth_app [in MetaRocq.PCUIC.Syntax.PCUICDepth]
term_forall_ctx_list_ind [in MetaRocq.PCUIC.Syntax.PCUICDepth]
term_forall_list_rect [in MetaRocq.Template.Induction]
term_forall_list_ind [in MetaRocq.Template.Induction]
term_subterm_redp [in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm_red1 [in MetaRocq.SafeChecker.PCUICWfReduction]
term_forall_list_ind [in MetaRocq.Erasure.EInduction]
term_on_free_vars_ind [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
term_noccur_between_list_ind [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
term_closedn_list_ind [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
test [in MetaRocq.Examples.tauto]
test_context_k_map [in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_context_k_mapi [in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_decl_map_decl [in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_context_k_app [in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_context_k_impl [in MetaRocq.PCUIC.utils.PCUICOnOne]
test_decl_conv_decls_map [in MetaRocq.PCUIC.PCUICConversion]
test_decl_map_decl [in MetaRocq.Common.BasicAst]
test_decl_impl [in MetaRocq.Common.BasicAst]
test_context_app [in MetaRocq.PCUIC.PCUICAst]
test_context_map [in MetaRocq.PCUIC.PCUICAst]
test_context_k_eq [in MetaRocq.PCUIC.PCUICAst]
test_context_k_eq_spec [in MetaRocq.PCUIC.PCUICAst]
test_context_k_eqP_eq_spec [in MetaRocq.PCUIC.PCUICAst]
test_context_k_eqP_id_spec [in MetaRocq.PCUIC.PCUICAst]
test_prim_eq_spec [in MetaRocq.PCUIC.PCUICAst]
test_prim_mapu [in MetaRocq.PCUIC.PCUICAst]
test_primu_test_primu_tPrimProp [in MetaRocq.PCUIC.PCUICAst]
test_prim_primProp [in MetaRocq.PCUIC.PCUICAst]
test_primu_test_primu_tPrimProp [in MetaRocq.PCUIC.PCUICWfUniverses]
test_context_k_ctx [in MetaRocq.PCUIC.PCUICWfUniverses]
test_context_mapi [in MetaRocq.PCUIC.PCUICWfUniverses]
test_primu_primProp [in MetaRocq.PCUIC.PCUICWfUniverses]
test_primu_mapu [in MetaRocq.PCUIC.PCUICWfUniverses]
test_context_k_closed_on_free_vars_ctx [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_k_on_free_vars_ctx [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_k_ctx [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
test_primIn_spec [in MetaRocq.Erasure.EPrimitive]
test_prim_eq_prop [in MetaRocq.Erasure.EPrimitive]
test_prim_map [in MetaRocq.Erasure.EPrimitive]
test_prim_impl_primProp [in MetaRocq.Erasure.EPrimitive]
test_prim_primProp [in MetaRocq.Erasure.EPrimitive]
test2 [in MetaRocq.Examples.tauto]
tfix_map_spec [in MetaRocq.Common.BasicAst]
tfix_forallb_map_spec [in MetaRocq.Template.Ast]
to_extended_list_case_branch_context [in MetaRocq.PCUIC.PCUICSR]
to_extended_list_set_binder_name [in MetaRocq.PCUIC.PCUICSR]
to_extended_list_k_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
to_extended_list_k_map_subst [in MetaRocq.PCUIC.PCUICSubstitution]
to_Z_bounded_bool [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
to_extended_list_k_cons [in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_lift_above [in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_spec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_length [in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_map_subst [in MetaRocq.Template.EtaExpand]
to_extended_list_smash_context_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
to_extended_list_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
to_extended_list_subst_context_let_expand [in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_length [in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_lift_context [in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_fold_context_k [in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_app [in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_expand_lets [in MetaRocq.PCUIC.PCUICInductives]
to_extended_list_k_map_lift [in MetaRocq.PCUIC.PCUICInductives]
to_extended_list_map_lift [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
to_extended_list_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
to_N_inj [in MetaRocq.Utils.bytestring]
tPrimProp_prod [in MetaRocq.PCUIC.PCUICAst]
tPrimProp_impl [in MetaRocq.PCUIC.PCUICAst]
tProd_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICConversion]
transform_wellformed_decl' [in MetaRocq.Erasure.EImplementBox]
transform_wellformed' [in MetaRocq.Erasure.EImplementBox]
transform_erasure_pipeline_function' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_erasure_pipeline_function [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_erase_pres_term [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_lambdabox_pres_term [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_lambda_box_eta_app [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_lambda_box_firstorder [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_compose_assoc [in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_blocks_eval [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_wf_global [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_env_extends [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_decl_extends [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_extends [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_wellformed_decl [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_wellformed [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_declared_constant [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_isLazyApp [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_isPrimApp [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_isConstructApp [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_tApp [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_nth [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_cunfold_cofix [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_cunfold_fix [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_cofix_subst [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_fix_subst [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_iota_red [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_substl [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_csubst [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps_eta_fn [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps_eta [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_decompose [in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps [in MetaRocq.Erasure.EConstructorsAsBlocks]
trans_eq_context_upto_names [in MetaRocq.PCUIC.PCUICEquality]
trans_lookup_projection [in MetaRocq.Erasure.ErasureProperties]
trans_lookup_constructor [in MetaRocq.Erasure.ErasureProperties]
trans_lookup_inductive [in MetaRocq.Erasure.ErasureProperties]
trans_lookup_constant [in MetaRocq.Erasure.ErasureProperties]
trans_env_remove_match_on_box_env [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
trans_env_fresh_globals [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
trans_env_fresh_global [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
trans_firstorder_ind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_firstorder_env [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_firstorder_mutind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_axiom_free [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ne_nf [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_case_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isFix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isRel [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isConstruct [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wcbveval [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_closedn [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_csubst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_ext [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_udecl [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_projs [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_type_local_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul_ctx_rel' [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_convSpec' [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_conv' [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul' [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul_ctx_rel [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_convSpec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumulSpec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_realargs [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_destArity [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_concl_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ctx_inst_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_subst_telescope [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_constraints [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_levels [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_prim_ty [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_branch_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_telescope [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_arities_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_predicate [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_annots [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_type_of_constructor [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_branch_type [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_cofixpoint [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_fixpoint [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_rec_kind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_one_cofix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_one_fix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_decompose_app [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_destInd [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_nisApp [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isApp [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_decompose_prod_assum [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mfix_All [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_branches [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_local_env [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_local' [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_conv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_leq_term [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_compare_term [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_term_upto_univ [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_context_upto_names [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_context_upto_names_eq_binder_annot [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cmp_global_instance [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_red1 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_untyped_subslet [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_is_closed_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_bbody [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_bcontext [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_binder_annot [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_predicate_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_set_binder_name_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_set_binder [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_set_binder [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_predicate_context_eq [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_predicate_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_to_extended_list [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_reln [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_inst_case_branch_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_inst_case_branch_context_gen [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_assumption_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context_inst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_k [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_extended_subst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_smash_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift_decl [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_decl [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_fix_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_is_constructor [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_unfold_cofix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_unfold_fix [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isLambda [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_nth [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_destr_arity [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_projection [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_inds [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_dbody [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_dtype [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_type [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cst_type [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_instance_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_instance [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst10 [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_decl_type [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mkApps [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_constructor [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_inductive [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_consistent_instance_ext [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_constraintSet_in [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_constant [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lookup [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_in_level_set [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mem_level_set [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_ext_constraints [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_ext_levels [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_free_vars_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_free_vars [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_app [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wcbvEval [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_cunfold_cofix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_cunfold_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_cofix_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_fix_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_substl [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_csubst [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_env_erase_global_decls [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
trans_red [in MetaRocq.PCUIC.PCUICReduction]
trans_env_debox [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
trans_subst_instance_decl [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_case_branch_type [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_it_mkLambda_or_LetIn [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_cofixpoint [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_fixpoint [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_check_rec_kind [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_check_one_cofix [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_check_one_fix [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_decompose_app [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_destInd [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_nisApp [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_isApp [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_decompose_prod_assum [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mfix_All2 [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mfix_All [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_branches [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_local_env [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_local' [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cumul [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_leq_term [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_eq_term_upto_univ [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_eq_context_gen_eq_binder_annot [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cmp_global_instance [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_red1 [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_bcontext [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_eq_binder_annot [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_case_predicate_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_local_set_binder_name_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_local_set_binder [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_set_binder [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_ind_predicate_context_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_ind_predicate_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_to_extended_list [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_reln [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_inst_case_branch_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context_inst [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_inds [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_expand_lets_ctx [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_expand_lets [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_expand_lets_k [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_extended_subst [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_smash_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_lift_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_fix_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_is_constructor [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_unfold_cofix [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_unfold_fix [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_isLambda [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_nth [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_it_mkProd_or_LetIn [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mkProd_or_LetIn [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_destr_arity [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_projection [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_dbody [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_dtype [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_type_of_constructor [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_ind_type [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cst_type [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst_instance_ctx [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst_instance [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst10 [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_decl_type [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mkApps [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_constructor [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_inductive [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_consistent_instance_ext [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_constraintSet_in [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_constant [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_lookup [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_in_level_set [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mem_level_set [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_global_ext_constraints [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_global_ext_levels [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_lift [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_local_app [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_on_global_env [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_consistent_instance_ext_gen [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_env_env_retroknowledge [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_env_env_universes [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_projs [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_ind_sorts [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_type_local_ctx [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_respects_variance [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cstr_respects_variance [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_arities [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumul_ctx_rel [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_closedn [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst_telescope [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_arities_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_env_retroknowledge [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_sort [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_case_branch_type [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumulSpec_typed [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumulSpec [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_consistent_instance_ext [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_decl_universes [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_cofixpoint [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_fixpoint [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_rec_kind [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_one_cofix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_one_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decompose_prod_assum [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decompose_app [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_local_env [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_local [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumul_gen [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_red1 [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_case_branch_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cstr_branch_context_alpha [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_predicate_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_case_predicate_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_app [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_inst_case_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_is_constructor [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_unfold_cofix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_unfold_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_isLambda [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_iota_red [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cstr_branch_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_smash_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_expand_lets_ctx [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lift_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_expand_lets [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_expand_lets_k [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_extended_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_nth [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_eq_term_list [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_eq_term [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_leq_term [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_eq_term_upto_univ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cmp_global_instance [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_to_extended_list [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_reln [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_npars [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_params_length [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_bodies_length [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_bodies [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_params [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_subst_instance [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_it_mkLambda_or_LetIn [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_it_mkProd_or_LetIn [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_inds [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_destArity [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst_instance [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_mkApp [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lift [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_decl_weaken [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_body_weakening [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_weakening [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_length [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decl_weakening [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_weakening [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup_env [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_decls_app [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup_inductive [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup_minductive [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_env_cons [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
trans_expanded [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
trans_template_program_wt [in MetaRocq.TemplatePCUIC.PCUICTransform]
trans_env_wf [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_decl_wf [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_wellformed_decl_irrel [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_wellformed_irrel [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_wellformed [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_expanded [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_eq [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_extends' [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded_decl_irrel [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded_decl [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded_irrel [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_correct [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_nth [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_cunfold_fix [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_fix_subst [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_iota_red [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_substl [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_csubst [in MetaRocq.Erasure.ECoInductiveToInductive]
trans_mkApps [in MetaRocq.Erasure.ECoInductiveToInductive]
triangle [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
triangle_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
tsize_downlift_le [in MetaRocq.Examples.tauto]
tsize_downlift [in MetaRocq.Examples.tauto]
tsize_lift [in MetaRocq.Examples.tauto]
tsize_decompose_app [in MetaRocq.Examples.tauto]
tsize_nonzero [in MetaRocq.Examples.tauto]
TT_typing_spine_app [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typecheck_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
typed_subst [in MetaRocq.PCUIC.PCUICSubstitution]
typed_subst_abstract_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
typed_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
type_local_ctx_Pclosed [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
type_local_ctx_All_local_env [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
type_reduction_closed [in MetaRocq.PCUIC.PCUICSR]
type_reduction [in MetaRocq.PCUIC.PCUICSR]
type_Cumul_alt [in MetaRocq.PCUIC.PCUICSR]
type_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICGeneration]
type_mkApps [in MetaRocq.PCUIC.PCUICGeneration]
type_mkApps [in MetaRocq.PCUIC.PCUICSpine]
type_it_mkProd_or_LetIn_inv [in MetaRocq.PCUIC.PCUICSpine]
type_Cumul' [in MetaRocq.PCUIC.PCUICTyping]
type_Prop [in MetaRocq.PCUIC.PCUICTyping]
type_Prop_wf [in MetaRocq.PCUIC.PCUICTyping]
type_closed_subst [in MetaRocq.Erasure.ErasureProperties]
type_inst [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
type_mkApps_arity [in MetaRocq.PCUIC.PCUICValidity]
type_App' [in MetaRocq.PCUIC.PCUICValidity]
type_ctx_wf_univ [in MetaRocq.PCUIC.PCUICValidity]
type_it_mkProd_or_LetIn_smash_middle [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
type_mkApps_napp [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
type_tCoFix_inv [in MetaRocq.PCUIC.PCUICInductiveInversion]
type_tFix_inv [in MetaRocq.PCUIC.PCUICInductiveInversion]
type_it_mkProd_or_LetIn_sorts [in MetaRocq.PCUIC.PCUICArities]
type_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICArities]
type_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICArities]
type_ws_cumul_pb [in MetaRocq.PCUIC.PCUICArities]
type_local_ctx_instantiate [in MetaRocq.PCUIC.PCUICContexts]
type_local_ctx_wf_local [in MetaRocq.PCUIC.PCUICContexts]
type_smash [in MetaRocq.SafeChecker.PCUICSafeChecker]
type_Prop_wf [in MetaRocq.Template.Typing]
type_Prop [in MetaRocq.Template.Typing]
type_local_ctx_wf [in MetaRocq.PCUIC.PCUICInductives]
type_local_ctx_cum [in MetaRocq.PCUIC.PCUICInductives]
type_mkApps_tConstruct_n_conv_arity [in MetaRocq.Erasure.EArities]
type_local_ctx_wf [in MetaRocq.PCUIC.PCUICWfUniverses]
type_app [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_mkApps_napp [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_is_open_term [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
type_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
type_Case_simple_subst_helper [in MetaRocq.PCUIC.PCUICCasesHelper]
type_Case_subst_helper [in MetaRocq.PCUIC.PCUICCasesHelper]
type_Case_helper [in MetaRocq.PCUIC.PCUICCasesHelper]
typing_renaming_cond_P [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
typing_closed_red [in MetaRocq.PCUIC.PCUICSR]
typing_closed_red1 [in MetaRocq.PCUIC.PCUICSR]
typing_spine_eval [in MetaRocq.Erasure.Prelim]
typing_spine_wt [in MetaRocq.Erasure.Prelim]
typing_spine_inv [in MetaRocq.Erasure.Prelim]
typing_spine_proofs [in MetaRocq.PCUIC.PCUICElimination]
typing_spine_it_mkProd_or_LetIn_full_inv [in MetaRocq.PCUIC.PCUICElimination]
typing_spine_case_predicate [in MetaRocq.PCUIC.PCUICElimination]
typing_spine_ctx_inst_smash [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_nth_error [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_app [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_ctx_inst [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_inv [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_wf_local [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_close [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_close_make_subst [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn' [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_gen [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_refl [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_strengthen [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_eq [in MetaRocq.PCUIC.PCUICSpine]
typing_spine_arity_spine [in MetaRocq.PCUIC.PCUICFirstorder]
typing_ind_env [in MetaRocq.PCUIC.PCUICTyping]
typing_ind_env_app_size [in MetaRocq.PCUIC.PCUICTyping]
typing_wf_local_size [in MetaRocq.PCUIC.PCUICTyping]
typing_wf_local [in MetaRocq.PCUIC.PCUICTyping]
typing_size_pos [in MetaRocq.PCUIC.PCUICTyping]
typing_wellformed [in MetaRocq.Erasure.ErasureProperties]
typing_inst [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
typing_rename [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
typing_rename_P [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
typing_rename_prop [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
typing_wf_fixpoint [in MetaRocq.Template.EtaExpand]
typing_spine_wt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
typing_subst_instance_decl [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance_ctx [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance'' [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance_wf_local [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance' [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_spine_to_extended_list_k_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
typing_spine_to_extended_list_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
typing_spine_isType_dom [in MetaRocq.PCUIC.PCUICArities]
typing_spine_WAT_concl [in MetaRocq.PCUIC.PCUICArities]
typing_spine_prod [in MetaRocq.PCUIC.PCUICArities]
typing_spine_weaken_concl [in MetaRocq.PCUIC.PCUICArities]
typing_spine_letin [in MetaRocq.PCUIC.PCUICArities]
typing_spine_letin_inv [in MetaRocq.PCUIC.PCUICArities]
typing_spine_isType_codom [in MetaRocq.PCUIC.PCUICArities]
typing_alpha [in MetaRocq.PCUIC.PCUICAlpha]
typing_alpha_prop [in MetaRocq.PCUIC.PCUICAlpha]
typing_spine_isArity [in MetaRocq.ErasurePlugin.ErasureCorrectness]
typing_expand_lets [in MetaRocq.PCUIC.PCUICContexts]
typing_spine_it_mkProd_or_LetIn_ext_list_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_it_mkProd_or_LetIn_ext_list_inv_gen [in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_prod_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_letin_inv' [in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_it_mkProd_or_LetIn_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_value_head [in MetaRocq.PCUIC.PCUICProgress]
typing_value_head_napp [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_prim_type [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_axiom [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_sort [in MetaRocq.PCUIC.PCUICProgress]
typing_constructor_arity [in MetaRocq.PCUIC.PCUICProgress]
typing_constructor_arity_exact [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_length [in MetaRocq.PCUIC.PCUICProgress]
typing_ind_env [in MetaRocq.PCUIC.PCUICProgress]
typing_ind_env_app_size [in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_strengthen [in MetaRocq.PCUIC.PCUICProgress]
typing_ind_env [in MetaRocq.Template.Typing]
typing_wf_local_size [in MetaRocq.Template.Typing]
typing_wf_local [in MetaRocq.Template.Typing]
typing_size_pos [in MetaRocq.Template.Typing]
typing_ws_cumul_pb [in MetaRocq.PCUIC.PCUICInversion]
typing_closed_ctx [in MetaRocq.PCUIC.PCUICInversion]
typing_infer_ind [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infer_prod [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infering_sort [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_checking [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infering [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_expand_lets_gen [in MetaRocq.PCUIC.PCUICInductives]
typing_spine_to_extended_list [in MetaRocq.PCUIC.PCUICInductives]
typing_cumul_term_prop [in MetaRocq.PCUIC.PCUICCumulProp]
typing_leq_term_prop [in MetaRocq.PCUIC.PCUICCumulProp]
typing_leq_term_prop_gen [in MetaRocq.PCUIC.PCUICCumulProp]
typing_wf [in MetaRocq.Template.TypingWf]
typing_wf_sigma [in MetaRocq.Template.TypingWf]
typing_all_wf_decl [in MetaRocq.Template.TypingWf]
typing_wf_gen [in MetaRocq.Template.TypingWf]
typing_cofix_coind [in MetaRocq.PCUIC.PCUICClassification]
typing_evar [in MetaRocq.PCUIC.PCUICClassification]
typing_var [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_nth_error_None_prod [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_nth_error_None [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_more_inv [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_all_inv [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_nth_error [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_smash [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_arity_mkApps_Ind [in MetaRocq.PCUIC.PCUICClassification]
typing_spine_inj [in MetaRocq.Erasure.EArities]
typing_spine_wat [in MetaRocq.Erasure.EArities]
typing_spine_Is_conv_to_Arity [in MetaRocq.Erasure.EArities]
typing_spine_mkApps_Ind_ex [in MetaRocq.Erasure.EArities]
typing_spine_red [in MetaRocq.Erasure.EArities]
typing_wf_sort [in MetaRocq.PCUIC.PCUICWfUniverses]
typing_wf_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
typing_eq_term [in MetaRocq.PCUIC.PCUICPrincipality]
typing_leq_term [in MetaRocq.PCUIC.PCUICPrincipality]
typing_spine_app [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_weaken_concl_size [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_weaken_concl [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_wf_wf [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
typing_closed_context [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
typwt [in MetaRocq.Erasure.Typed.Erasure]
tywt [in MetaRocq.Erasure.Typed.Erasure]
| 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) |