| 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) |
W
wat_welltyped [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]Wcbv [section, in MetaRocq.Template.WcbvEval]
Wcbv [section, in MetaRocq.Erasure.EWcbvEval]
Wcbv [section, in MetaRocq.Erasure.EWcbvEval]
Wcbv [section, in MetaRocq.Erasure.EWcbvEvalNamed]
Wcbv [section, in MetaRocq.PCUIC.PCUICWcbvEval]
WcbvEnv [section, in MetaRocq.Erasure.EWcbvEval]
WcbvEnv.efl [variable, in MetaRocq.Erasure.EWcbvEval]
WcbvEnv.wfl [variable, in MetaRocq.Erasure.EWcbvEval]
WcbvEval [library]
WcbvEvalAux [library]
wcbveval_red [lemma, in MetaRocq.PCUIC.PCUICClassification]
WcbvFlags [record, in MetaRocq.Erasure.EWcbvEval]
wcbv_standardization_fst [lemma, in MetaRocq.PCUIC.PCUICNormalization]
wcbv_standardization [lemma, in MetaRocq.PCUIC.PCUICNormalization]
wcbv_normalization [lemma, in MetaRocq.PCUIC.PCUICNormalization]
wcbv_red1_mkApps_left [lemma, in MetaRocq.PCUIC.PCUICProgress]
wcbv_red1_eval [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_red1 [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_closed [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_sind [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_rec [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_ind [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_rect [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_array_value [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_array_default [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_cofix_case [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_cofix_proj [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_fix [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_proj [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_proj_in [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_iota [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_case_in [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_delta [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_zeta [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_let_in [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_beta [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_app_right [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red_app_left [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1 [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
Wcbv.map_eval_prim.F [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.P [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.eval [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.term' [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.term [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim [section, in MetaRocq.Erasure.EWcbvEval]
Wcbv.wfl [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.wfl [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.Σ [variable, in MetaRocq.Template.WcbvEval]
Wcbv.Σ [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.Σ [variable, in MetaRocq.Erasure.EWcbvEval]
Wcbv.Σ [variable, in MetaRocq.Erasure.EWcbvEvalNamed]
Wcbv.Σ [variable, in MetaRocq.PCUIC.PCUICWcbvEval]
wcored [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
wcored_wf [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
weakening [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_env_normalization_in [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
weakening_closed_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
weakening_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICSR]
weakening_gen [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_length [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_typing [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_rename_typing [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local_eq [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_closed_red [lemma, in MetaRocq.PCUIC.PCUICSpine]
weakening_env_cumul_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_convSpec [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_gen [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_red1 [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_config_normalization_in [lemma, in MetaRocq.PCUIC.PCUICWeakeningConfigSN]
weakening_env_cored [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
weakening_env_declared_projection [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constructor [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_inductive [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_minductive [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constant [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_consistent_instance [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_is_allowed_elimination [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_constraints [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels' [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_cumulSpec0 [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
weakening_cumul0 [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
weakening_is_closed_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
weakening_env_declared_constructor [lemma, in MetaRocq.Erasure.EExtends]
weakening_env_declared_inductive [lemma, in MetaRocq.Erasure.EExtends]
weakening_env_declared_minductive [lemma, in MetaRocq.Erasure.EExtends]
weakening_env_declared_constant [lemma, in MetaRocq.Erasure.EExtends]
weakening_config_normalizing [instance, in MetaRocq.PCUIC.PCUICSN]
weakening_ws_cumul_pb_eq [lemma, in MetaRocq.PCUIC.PCUICConversion]
weakening_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
weakening_config_wf [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config_wf_local [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config_wf_local_sized [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config_consistent_instance [lemma, in MetaRocq.PCUIC.PCUICWeakeningConfig]
weakening_config_is_allowed_elimination [lemma, in MetaRocq.PCUIC.PCUICWeakeningConfig]
weakening_pred1_0 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
weakening_pred1_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
weakening_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
weakening_eval_env [lemma, in MetaRocq.Erasure.EWcbvEval]
weakening_conv_wt [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_conv [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_cumul [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red_0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red' [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red1 [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_renaming [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_config_cumul_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_conv_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumul_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_conv_decls [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumulSpec [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_convSpec [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumulSpec0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumul [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_conv [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumul_gen [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_type_local_ctx [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
weakening_env_strictly_on_decls_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_strictly_decls_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_decls_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_gen_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_strictly_ext [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_strictly [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_ext [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl [definition, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_gen [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening0 [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
weaken_env_prop_closed [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
weaken_ctx [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_wf_local [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_subslet [lemma, in MetaRocq.PCUIC.PCUICSpine]
weaken_env_prop_strictly_on_decls_to_strictly_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_decls_to_strictly_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_to_strictly_on_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_to_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_strictly_on_decls_to_strictly_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_decls_to_strictly_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_to_strictly_on_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_to_decls [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_gen_impl [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_gen_impl [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_on_decls_prop [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_decls_prop [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_decls_prop [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_on_decls_prop_full [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_decls_prop_full [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_decls_prop_full [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_gen [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_gen [definition, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_lookup_on_global_env' [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_prefix [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
weaken_prop [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
weaken_prop_gen [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
weaken_wf_subslet [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
weaken_ws_cumul_ctx_pb_rel [lemma, in MetaRocq.PCUIC.PCUICConversion]
weaken_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
weaken_subslet [lemma, in MetaRocq.PCUIC.PCUICArities]
weaken_sorts_local_ctx [lemma, in MetaRocq.PCUIC.PCUICContexts]
weaken_type_local_ctx [lemma, in MetaRocq.PCUIC.PCUICContexts]
weaken_nth_error_lt [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_nth_error_ge [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_wf_universes [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_instance [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_level [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_universe [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_decl_pred [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
weaken_wf_local [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_prop_typing [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_decls_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_lookup_on_global_env [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
WeakEtaExp [section, in MetaRocq.Erasure.EEtaExpanded]
WeakEtaExp.Σ [variable, in MetaRocq.Erasure.EEtaExpanded]
WeightedGraph [module, in MetaRocq.Utils.wGraph]
WeightedGraphSig [module, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_relabel_on [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop_sloop [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_sloop [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_relabel [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_caract2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_caract1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_lsp0_xx [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_labelling [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop_loop' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop [record, in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop [inductive, in MetaRocq.Utils.wGraph]
WeightedGraph.add_end [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.add_edge [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.add_node [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Add_Add [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Add_In [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Add_Proper [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.Build_acyclic_no_loop [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.Build_acyclic_no_loop [constructor, in MetaRocq.Utils.wGraph]
WeightedGraph.concat [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling_lsp_G' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling_lsp [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling_PathOf [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.diff [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Disjoint [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_In [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add4 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove_inv [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Equal_l [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Equal [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove_add [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Proper [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_union [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Subset [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add3 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Disjoint_DisjointAdd [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.E [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge [module, in MetaRocq.Utils.wGraph]
WeightedGraph.EdgeOf [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.EdgeSet [module, in MetaRocq.Utils.wGraph]
WeightedGraph.EdgeSetDecide [module, in MetaRocq.Utils.wGraph]
WeightedGraph.EdgeSetFact [module, in MetaRocq.Utils.wGraph]
WeightedGraph.EdgeSetProp [module, in MetaRocq.Utils.wGraph]
WeightedGraph.edges_sub [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.edges_vertices [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.edge_map_spec2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.edge_map_spec1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.edge_map [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.edge_pathOf [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.compare [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.compare_spec [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eqb [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq_leibniz [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq_dec [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq_equiv [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.lt [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.lt_compat [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.lt_strorder [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.t [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling [section, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.acG2 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.embed [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.Gl [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.G1 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.G2 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.HGl [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.l [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.l' [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.extends_correct_labelling [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.extends_labelling [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.e_weight [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.e_target [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.e_source [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.FirstVertexIn [section, in MetaRocq.Utils.wGraph]
WeightedGraph.FirstVertexIn.G1 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.FirstVertexIn.G2 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.first_in_first [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.first_in_in [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.first_in [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_equiv [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_proper [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_filter [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_map [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.from_G'_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.from_G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.from_G'_path_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.from_G'_path [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.from1 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.from2 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.full_subgraph [record, in MetaRocq.Utils.wGraph]
WeightedGraph.graph [section, in MetaRocq.Utils.wGraph]
WeightedGraph.graph.G [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.graph.HI [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.HG' [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.HI' [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.invariants [record, in MetaRocq.Utils.wGraph]
WeightedGraph.invariants_relabel [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.In_nodes_app_end [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph [module, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.Border [section, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.Border.ext [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.Border.G1 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.EdgeSet_fold_spec_right2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_lsp_dominate [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder [section, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.bs [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.ext [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.G1 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.G2 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_eq_is_full_extension [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_bound_extend_border [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.spath_on_border [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.sweight_bound0 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.is_subgraph [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.is_acyclic_correct [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.is_acyclic_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.is_acyclic [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.is_nonpos_nbar [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.is_nonpos_spec [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.is_nonpos [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.is_simple [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.labelling [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.labelling_ext_lsp [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.length [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.leqb_vertices_correct [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.leqb_vertices [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.leq_vertices_caract [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.leq_vertices_caract0 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.leq_vertices [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.le_Some_lsp [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_dominate [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_Gl_between_G1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_Gl_upperbound_G1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_edge [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_map_path2 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_vset_in [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_spec_left [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_incr [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_sx [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_yx [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_pathOf [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_source_max [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_to_source [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_from_source [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_xx [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_xx_acyclic [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_to_s [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_sym [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_codistance [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_correctness [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_s [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_optim [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_fast [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_sub [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_triangle_inequality [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_spec_eq0 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_spec_eq [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_spec_le [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_VSet_Equal [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_eq [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp00 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp00_optim [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.lsp00_fast [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath [section, in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath.G1 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath.G2 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath.on_edge [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.map_spath [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.map_path [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.negbe [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.nodes [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.nodes_subset [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.opp_edge [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf [inductive, in MetaRocq.Utils.wGraph]
WeightedGraph.pathOf_add_end_simpl [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_add_end_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_add_end [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_In [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_sind [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_rec [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_ind [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_rect [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.pathOf_step [constructor, in MetaRocq.Utils.wGraph]
WeightedGraph.pathOf_refl [constructor, in MetaRocq.Utils.wGraph]
WeightedGraph.PosPathOf [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.reduce [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.reflectEq_nbar [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.reflectEq_Z [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.reflectEq_vertices [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.reflect_logically_equiv [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn [section, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.embed [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.Gl [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.G1 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.G2 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.HGl [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.l [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.preserves_edges [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge [module, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy_bound [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_diff [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_y [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_x [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_correct [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.r [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge [section, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.acG [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling [section, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.d [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.Hk [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.Hl [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.k [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.l [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.x [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.G [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.invG [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs [section, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.hx [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.hxy [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.hy [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.nxy [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.x [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.y [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.r_correct [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.stdl [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_mon [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_add [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_correct_labelling [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_invariants [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_lsp_G2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_lsp_G1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_map [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_path [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_lsp [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux3 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.s [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.same_src [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.sconcat [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.simplify [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.simplify_aux3 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.simplify_aux2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.simplify_aux1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.simplify2 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.simplify2' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.snodes [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.snodes_Subset [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.source_bottom [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.source_pathOf [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.source_vertex [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath [inductive, in MetaRocq.Utils.wGraph]
WeightedGraph.spathG1_lsp_Gl [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_sets [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_In' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_In [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.spath_one [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_sub [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_sind [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_rec [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_ind [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_rect [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.spath_step [constructor, in MetaRocq.Utils.wGraph]
WeightedGraph.spath_refl [constructor, in MetaRocq.Utils.wGraph]
WeightedGraph.split [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.split' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.sto_G'_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.sto_G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph [record, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph [section, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph_acyclic [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph_on_edge [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.G [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.HG [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.HI [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2 [section, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.Hxs [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.K [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.Vx [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.Vy [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.x_0 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.y_0 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1 [module, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.correct_labelling_lsp_G' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G'_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2 [section, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.G [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.HG [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.HI [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.Hxs [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.K [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.Vx [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.Vy [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.x_0 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.y_0 [variable, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.HG' [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.HI' [instance, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_spec_left [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_sx [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_incr [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_yx [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_pathOf [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.sto_G'_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.sto_G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.to_G'_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.to_G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.succs [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.sweight [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_relabel_on_G2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_relabel_on_G1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_inverse [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_sconcat [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.t [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.to_label_to_nat [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.to_G'_weight [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.to_G' [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.to_label_max [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.to_label [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.to_simple [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.to_pathOf [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.V [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.vertices_sub [projection, in MetaRocq.Utils.wGraph]
WeightedGraph.VSetDecide [module, in MetaRocq.Utils.wGraph]
WeightedGraph.VSetFact [module, in MetaRocq.Utils.wGraph]
WeightedGraph.VSetProp [module, in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_Forall_reflect [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_add_add_same [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_add_add [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_remove_add [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_add_remove [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_from2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_from1 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_spath2 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_spath1 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_path2 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_path1 [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_inverse [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_simplify2' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_simplify2 [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_reduce [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_simplify [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_split' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_split [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_SPath_sub [definition, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_add_end [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.weight_concat [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Zle_opp' [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Zle_opp [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Z_of_to_label_pos [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Z_of_to_label_s [lemma, in MetaRocq.Utils.wGraph]
WeightedGraph.Z_of_to_label [lemma, in MetaRocq.Utils.wGraph]
_ ..w [notation, in MetaRocq.Utils.wGraph]
_ ..t [notation, in MetaRocq.Utils.wGraph]
_ ..s [notation, in MetaRocq.Utils.wGraph]
wellformed [definition, in MetaRocq.Erasure.ErasureProperties]
wellformed [abbreviation, in MetaRocq.Erasure.EWellformed]
wellformed [definition, in MetaRocq.Erasure.EWellformed]
wellformed_lookup_constructor_pars_args [lemma, in MetaRocq.Erasure.EImplementBox]
wellformed_lookup_constructor_pars [lemma, in MetaRocq.Erasure.EImplementBox]
wellformed_lookup_inductive_pars [lemma, in MetaRocq.Erasure.EImplementBox]
wellformed_gen_transform_decl_extends [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
wellformed_gen_transform_extends [projection, in MetaRocq.Erasure.EGenericGlobalMap]
wellformed_gen_transform_extends [constructor, in MetaRocq.Erasure.EGenericGlobalMap]
wellformed_remove_match_on_box_decl_extends [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
wellformed_remove_match_on_box_extends [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
wellformed_gen_transform_decl_extends [lemma, in MetaRocq.Erasure.EGenericMapEnv]
wellformed_lookup_constructor_pars_args [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_constructor_pars [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_inductive_pars [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
wellformed_annotate [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
wellformed_annotate' [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
wellformed_closed_env [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_mkApps [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_iota_red_brs [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_iota_red [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_cunfold_cofix [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_cunfold_fix [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_cofix_subst [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_fix_subst [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_substl [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_csubst [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_subst [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_subst_eq [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_lift [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_up [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_closed_decl [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_closed [lemma, in MetaRocq.Erasure.EWellformed]
wellformed_optimize_decl_extends [lemma, in MetaRocq.Erasure.EInlineProjections]
wellformed_optimize_extends [lemma, in MetaRocq.Erasure.EInlineProjections]
wellformed_projection_args [lemma, in MetaRocq.Erasure.EInlineProjections]
wellformed_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_case_branch_body_rec [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_single [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_trans_decl_extends [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
wellformed_trans_extends [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
wellfounded [instance, in MetaRocq.SafeChecker.PCUICSafeReduce]
WellFounded_erase_rel [instance, in MetaRocq.Erasure.Typed.Erasure]
wellinferred [inductive, in MetaRocq.SafeChecker.PCUICSafeRetyping]
wellinferred_sind [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
wellinferred_ind [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
wellscoped [section, in MetaRocq.Erasure.ErasureProperties]
wellscoped.Def [section, in MetaRocq.Erasure.ErasureProperties]
wellscoped.Def.Σ [variable, in MetaRocq.Erasure.ErasureProperties]
welltyped [abbreviation, in MetaRocq.PCUIC.PCUICSR]
welltyped [inductive, in MetaRocq.PCUIC.PCUICTyping]
welltyped_terms [abbreviation, in MetaRocq.PCUIC.PCUICSR]
welltyped_R_pres [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
welltyped_is_open_term [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
welltyped_is_closed_context [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
welltyped_brs [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_zipp [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_stack_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_zipx [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn_iff [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_fill_context_hole [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_alpha [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_sind [definition, in MetaRocq.PCUIC.PCUICTyping]
welltyped_ind [definition, in MetaRocq.PCUIC.PCUICTyping]
welltyped_wellformed [lemma, in MetaRocq.Erasure.ErasureProperties]
welltyped_subterm [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
welltyped_mkApps_inv [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
welltyped_mkApps_inv [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
welltyped_letin_red [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
welltyped_letin_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
welltyped_prod_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
welltyped_R_zipc [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_wf [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipp_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tProd_appstack_nil [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tCase_brs_length [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tConst_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_wf_local [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
well_founded_erase_rel [lemma, in MetaRocq.Erasure.Typed.Erasure]
well_founded_term_sub_ctx [lemma, in MetaRocq.Erasure.Typed.Erasure]
well_typed [definition, in MetaRocq.Erasure.Prelim]
well_prop_wf [lemma, in MetaRocq.Examples.tauto]
well_prop_sind [definition, in MetaRocq.Examples.tauto]
well_prop_rec [definition, in MetaRocq.Examples.tauto]
well_prop_ind [definition, in MetaRocq.Examples.tauto]
well_prop_rect [definition, in MetaRocq.Examples.tauto]
well_prop_True [constructor, in MetaRocq.Examples.tauto]
well_prop_False [constructor, in MetaRocq.Examples.tauto]
well_prop_Or [constructor, in MetaRocq.Examples.tauto]
well_prop_And [constructor, in MetaRocq.Examples.tauto]
well_prop_Impl [constructor, in MetaRocq.Examples.tauto]
well_prop_Rel [constructor, in MetaRocq.Examples.tauto]
well_prop [inductive, in MetaRocq.Examples.tauto]
well_subst_closed_subst [definition, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
well_subst_usubst [definition, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
well_sorted_wellinferred [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
well_sorted [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
well_subst [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
well_subst_app_up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up' [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
weqt [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
wf [definition, in MetaRocq.PCUIC.PCUICTyping]
wf [inductive, in MetaRocq.Template.WfAst]
wf [definition, in MetaRocq.Template.Typing]
wf [inductive, in MetaRocq.Erasure.EWcbvEvalNamed]
wf [section, in MetaRocq.Erasure.EWellformed]
WfArity_build_case_predicate_type [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
WfAst [section, in MetaRocq.Template.TypingWf]
WfAst [library]
WfAst.cf [variable, in MetaRocq.Template.TypingWf]
WfAst.Σ [variable, in MetaRocq.Template.TypingWf]
WfEnv [section, in MetaRocq.PCUIC.PCUICSpine]
WfEnv [section, in MetaRocq.PCUIC.PCUICSpine]
WfEnv [section, in MetaRocq.PCUIC.PCUICArities]
WfEnv [section, in MetaRocq.PCUIC.PCUICContexts]
WfEnv [section, in MetaRocq.PCUIC.PCUICProgress]
WfEnv [section, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
WfEnv.cf [variable, in MetaRocq.PCUIC.PCUICSpine]
WfEnv.cf [variable, in MetaRocq.PCUIC.PCUICSpine]
WfEnv.cf [variable, in MetaRocq.PCUIC.PCUICArities]
WfEnv.cf [variable, in MetaRocq.PCUIC.PCUICContexts]
WfEnv.cf [variable, in MetaRocq.PCUIC.PCUICProgress]
WfEnv.cf [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
WfEnv.guard [variable, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
WfEnv.wfΣ [variable, in MetaRocq.PCUIC.PCUICSpine]
WfEnv.wfΣ [variable, in MetaRocq.PCUIC.PCUICSpine]
WfEnv.wfΣ [variable, in MetaRocq.PCUIC.PCUICArities]
WfEnv.wfΣ [variable, in MetaRocq.PCUIC.PCUICContexts]
WfEnv.wfΣ [variable, in MetaRocq.PCUIC.PCUICProgress]
WfEnv.Σ [variable, in MetaRocq.PCUIC.PCUICSpine]
WfEnv.Σ [variable, in MetaRocq.PCUIC.PCUICSpine]
WfEnv.Σ [variable, in MetaRocq.PCUIC.PCUICArities]
WfEnv.Σ [variable, in MetaRocq.PCUIC.PCUICContexts]
WfEnv.Σ [variable, in MetaRocq.PCUIC.PCUICProgress]
wffix [section, in MetaRocq.Erasure.ErasureFunctionProperties]
WfLookup [section, in MetaRocq.Template.TypingWf]
WfLookup.cf [variable, in MetaRocq.Template.TypingWf]
WfLookup.Σ [variable, in MetaRocq.Template.TypingWf]
wfl_size_rel [abbreviation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
wfl_size [abbreviation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
WfRed [section, in MetaRocq.Template.TypingWf]
WfRed.cf [variable, in MetaRocq.Template.TypingWf]
WfRed.Σ [variable, in MetaRocq.Template.TypingWf]
wfterm [definition, in MetaRocq.Template.TemplateCheckWf]
wf_fresh_globals [lemma, in MetaRocq.Template.TemplateEnvMap]
wf_pop_decl [lemma, in MetaRocq.Erasure.Typed.Erasure]
wf_local_subst1 [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_local_red [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_local_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_local_isType_nth [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_subslet_skipn [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_pre_case_branch_context [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_cofixpoint_red1_body [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_cofixpoint_red1_type [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_fixpoint_red1_body [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_fixpoint_red1_type [lemma, in MetaRocq.PCUIC.PCUICSR]
wf_proof [instance, in MetaRocq.SafeChecker.PCUICSafeReduce]
wf_arities_context [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
wf_arities_context' [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
wf_ext_wf [lemma, in MetaRocq.PCUIC.PCUICElimination]
wf_local_nth_isType [lemma, in MetaRocq.PCUIC.PCUICSpine]
wf_arity_spine_typing_spine [lemma, in MetaRocq.PCUIC.PCUICSpine]
wf_arity_spine_spine [projection, in MetaRocq.PCUIC.PCUICSpine]
wf_arity_spine_wf [projection, in MetaRocq.PCUIC.PCUICSpine]
wf_arity_spine [record, in MetaRocq.PCUIC.PCUICSpine]
wf_local_alpha [lemma, in MetaRocq.PCUIC.PCUICSpine]
wf_reduction [instance, in MetaRocq.Erasure.ErasureFunction]
wf_reduction_aux [definition, in MetaRocq.Erasure.ErasureFunction]
wf_cod' [lemma, in MetaRocq.Erasure.ErasureFunction]
wf_cod [lemma, in MetaRocq.Erasure.ErasureFunction]
wf_global_decl_deps [lemma, in MetaRocq.Erasure.ErasureFunction]
wf_local_rel_alpha_eq_end [lemma, in MetaRocq.Erasure.ErasureFunction]
wf_fun [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
wf_case_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
wf_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
wf_local_All_fold [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wf_local_inv [lemma, in MetaRocq.PCUIC.PCUICTyping]
wf_local_app_l [lemma, in MetaRocq.PCUIC.PCUICTyping]
wf_ext_consistent [lemma, in MetaRocq.PCUIC.PCUICTyping]
wf_ext_wf [lemma, in MetaRocq.PCUIC.PCUICTyping]
wf_ext [definition, in MetaRocq.PCUIC.PCUICTyping]
wf_env_non_var_levels [lemma, in MetaRocq.PCUIC.PCUICTyping]
wf_cofixpoint [definition, in MetaRocq.PCUIC.PCUICTyping]
wf_cofixpoint_gen [definition, in MetaRocq.PCUIC.PCUICTyping]
wf_fixpoint [definition, in MetaRocq.PCUIC.PCUICTyping]
wf_fixpoint_gen [definition, in MetaRocq.PCUIC.PCUICTyping]
wf_ext_gc_of_uctx_irr [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
wf_ext_gc_of_uctx [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
wf_gc_of_uctx [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
wf_brs [definition, in MetaRocq.Erasure.ErasureProperties]
wf_local_rel_conv [lemma, in MetaRocq.Erasure.ErasureProperties]
wf_local_app_renaming [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
wf_consistent [lemma, in MetaRocq.PCUIC.PCUICGlobalEnv]
wf_ext_global_uctx_invariants [definition, in MetaRocq.PCUIC.PCUICGlobalEnv]
wf_global_uctx_invariants [definition, in MetaRocq.PCUIC.PCUICGlobalEnv]
wf_cumul_context_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wf_conv_context_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
WF_precompose [instance, in MetaRocq.PCUIC.utils.PCUICUtils]
wf_dlexprod [lemma, in MetaRocq.PCUIC.utils.PCUICUtils]
wf_local_validity [lemma, in MetaRocq.PCUIC.PCUICValidity]
wf_pre_case_predicate_context_gen [lemma, in MetaRocq.PCUIC.PCUICValidity]
wf_lookup [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
wf_fixpoints [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
wf_fresh_globals [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
wf_fixpoint_rarg [lemma, in MetaRocq.Template.EtaExpand]
wf_cons_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_ind_indices [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_ext_trans [abbreviation, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_trans [abbreviation, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_local_ind_params_weaken [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_mkApps [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
wf_local_bd_rel_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_bd_typing [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_local_rel [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_rel_weak [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_rel_subst1 [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_subst_instance_decl [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate_poly [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_case_branches_types' [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_branches_types [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type' [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_pre_case_branch_context_gen [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_predicate_context [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_local_vass [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_typing_spine [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_all [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_cunfold_cofix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_cunfold_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_cofix_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_fix_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_substl [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_csubst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_nth [lemma, in MetaRocq.Template.WfAst]
wf_subst_instance [lemma, in MetaRocq.Template.WfAst]
wf_mkApps_inv [lemma, in MetaRocq.Template.WfAst]
wf_mkApps_napp [lemma, in MetaRocq.Template.WfAst]
wf_strip_outer_cast [lemma, in MetaRocq.Template.WfAst]
wf_subst1 [lemma, in MetaRocq.Template.WfAst]
wf_subst [lemma, in MetaRocq.Template.WfAst]
wf_lift [lemma, in MetaRocq.Template.WfAst]
wf_mkApps [lemma, in MetaRocq.Template.WfAst]
wf_mkApp [lemma, in MetaRocq.Template.WfAst]
wf_decl_pred [definition, in MetaRocq.Template.WfAst]
wf_decl [definition, in MetaRocq.Template.WfAst]
wf_inv [lemma, in MetaRocq.Template.WfAst]
wf_Inv [definition, in MetaRocq.Template.WfAst]
wf_sind [definition, in MetaRocq.Template.WfAst]
wf_rec [definition, in MetaRocq.Template.WfAst]
wf_ind [definition, in MetaRocq.Template.WfAst]
wf_rect [definition, in MetaRocq.Template.WfAst]
wf_tArray [constructor, in MetaRocq.Template.WfAst]
wf_tString [constructor, in MetaRocq.Template.WfAst]
wf_tFloat [constructor, in MetaRocq.Template.WfAst]
wf_tInt [constructor, in MetaRocq.Template.WfAst]
wf_tCoFix [constructor, in MetaRocq.Template.WfAst]
wf_tFix [constructor, in MetaRocq.Template.WfAst]
wf_tProj [constructor, in MetaRocq.Template.WfAst]
wf_tCase [constructor, in MetaRocq.Template.WfAst]
wf_tConstruct [constructor, in MetaRocq.Template.WfAst]
wf_tInd [constructor, in MetaRocq.Template.WfAst]
wf_tConst [constructor, in MetaRocq.Template.WfAst]
wf_tApp [constructor, in MetaRocq.Template.WfAst]
wf_tLetIn [constructor, in MetaRocq.Template.WfAst]
wf_tLambda [constructor, in MetaRocq.Template.WfAst]
wf_tProd [constructor, in MetaRocq.Template.WfAst]
wf_tCast [constructor, in MetaRocq.Template.WfAst]
wf_tSort [constructor, in MetaRocq.Template.WfAst]
wf_tEvar [constructor, in MetaRocq.Template.WfAst]
wf_tVar [constructor, in MetaRocq.Template.WfAst]
wf_tRel [constructor, in MetaRocq.Template.WfAst]
wf_nactx [abbreviation, in MetaRocq.Template.WfAst]
wf_local_def [lemma, in MetaRocq.PCUIC.PCUICArities]
wf_local_ass [lemma, in MetaRocq.PCUIC.PCUICArities]
wf_typing_spine [definition, in MetaRocq.PCUIC.PCUICArities]
wf_local_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
wf_local_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICAlpha]
wf_local_nth_error_vass [lemma, in MetaRocq.PCUIC.PCUICAlpha]
wf_glob_lookup_inductive_pars [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
wf_glob_fresh [lemma, in MetaRocq.Erasure.EProgram]
wf_eprogram_env [definition, in MetaRocq.Erasure.EProgram]
wf_eprogram [definition, in MetaRocq.Erasure.EProgram]
wf_local_smash_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
wf_local_rel_empty [lemma, in MetaRocq.PCUIC.PCUICContexts]
wf_local_smash_end [lemma, in MetaRocq.PCUIC.PCUICContexts]
wf_local_rel_smash_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
wf_local_rel_smash_context_gen [lemma, in MetaRocq.PCUIC.PCUICContexts]
wf_erase_global_decls_recursive [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_erase_global_decl [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_trans_inductives [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_squash [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_cs_sorts [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ctx_universes_app [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_local_wf_ctx_universes [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ctx_universes_subst_instance [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_decl_universes_subst_instance [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ind_types_wf_arities [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ind_types [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_env_check_ws_cumul_ctx [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_env_check_cumul_decl [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_env_conv [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_mkApps [lemma, in MetaRocq.Erasure.EGenericMapEnv]
wf_inductive_mapping_inv [lemma, in MetaRocq.Erasure.EReorderCstrs]
wf_mkApps [lemma, in MetaRocq.Erasure.EReorderCstrs]
wf_optimize [lemma, in MetaRocq.Erasure.EReorderCstrs]
wf_ind_mapping_wf_brs [lemma, in MetaRocq.Erasure.EReorderCstrs]
wf_glob_ind_projs [lemma, in MetaRocq.Erasure.EReorderCstrs]
wf_inductives_mapping [definition, in MetaRocq.Erasure.EReorderCstrs]
wf_inductive_mapping [definition, in MetaRocq.Erasure.EReorderCstrs]
wf_reordering [definition, in MetaRocq.Erasure.EReorderCstrs]
wf_tags_list [definition, in MetaRocq.Erasure.EReorderCstrs]
wf_tags [definition, in MetaRocq.Erasure.EReorderCstrs]
wf_program [definition, in MetaRocq.Template.TemplateCheckWf]
wf_global_env [definition, in MetaRocq.Template.TemplateCheckWf]
wf_global_declarations [definition, in MetaRocq.Template.TemplateCheckWf]
wf_global_decl [definition, in MetaRocq.Template.TemplateCheckWf]
wf_ext_wf [definition, in MetaRocq.Template.Typing]
wf_local_inv [lemma, in MetaRocq.Template.Typing]
wf_local_app_l [lemma, in MetaRocq.Template.Typing]
wf_ext [definition, in MetaRocq.Template.Typing]
wf_cofixpoint [definition, in MetaRocq.Template.Typing]
wf_fixpoint [definition, in MetaRocq.Template.Typing]
wf_inductive_mapping_trans [lemma, in MetaRocq.ErasurePlugin.Erasure]
wf_template_inductives_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
wf_template_inductive_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
wf_pcuic_inductives_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
wf_pcuic_inductive_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
wf_local_rel_wf_local_bd [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
wf_local_wf_local_bd [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
wf_ind_predicate [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_local_expand_lets [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_projection_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_projection_arg_ctx [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_projection_context_gen [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_subslet_dom [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_subslet_subslet [projection, in MetaRocq.PCUIC.PCUICInductives]
wf_subslet_ctx [projection, in MetaRocq.PCUIC.PCUICInductives]
wf_subslet [record, in MetaRocq.PCUIC.PCUICInductives]
wf_arities_context_inst [lemma, in MetaRocq.PCUIC.PCUICInductives]
wf_precompose [lemma, in MetaRocq.Utils.MRRelations]
wf_consistent_extension_on_consistent [lemma, in MetaRocq.SafeChecker.PCUICWfEnv]
wf_fix_env [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_add_multiple [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_vLazy [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_vPrim [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_vRecClos [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_vConstruct [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_vClos [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
wf_glob_sind [definition, in MetaRocq.Erasure.EWellformed]
wf_glob_ind [definition, in MetaRocq.Erasure.EWellformed]
wf_glob_cons [constructor, in MetaRocq.Erasure.EWellformed]
wf_glob_nil [constructor, in MetaRocq.Erasure.EWellformed]
wf_glob [inductive, in MetaRocq.Erasure.EWellformed]
wf_global_decl [definition, in MetaRocq.Erasure.EWellformed]
wf_minductive [definition, in MetaRocq.Erasure.EWellformed]
wf_inductive [definition, in MetaRocq.Erasure.EWellformed]
wf_projections [definition, in MetaRocq.Erasure.EWellformed]
wf_fix_inv [lemma, in MetaRocq.Erasure.EWellformed]
wf_fix [abbreviation, in MetaRocq.Erasure.EWellformed]
wf_brs [definition, in MetaRocq.Erasure.EWellformed]
wf_fix_gen [definition, in MetaRocq.Erasure.EWellformed]
wf_it_mkLambda_or_LetIn [lemma, in MetaRocq.Template.TypingWf]
wf_Lambda_or_LetIn [lemma, in MetaRocq.Template.TypingWf]
wf_it_mkProd_or_LetIn_inv [lemma, in MetaRocq.Template.TypingWf]
wf_lift_wf [lemma, in MetaRocq.Template.TypingWf]
wf_red1 [lemma, in MetaRocq.Template.TypingWf]
wf_projs [lemma, in MetaRocq.Template.TypingWf]
wf_ind_projs [projection, in MetaRocq.Template.TypingWf]
wf_ind_ctors_indices [projection, in MetaRocq.Template.TypingWf]
wf_ind_ctor_args [projection, in MetaRocq.Template.TypingWf]
wf_ind_ctors [projection, in MetaRocq.Template.TypingWf]
wf_ind_indices [projection, in MetaRocq.Template.TypingWf]
wf_ind_type [projection, in MetaRocq.Template.TypingWf]
wf_inductive_body [record, in MetaRocq.Template.TypingWf]
wf_case_branches_context [lemma, in MetaRocq.Template.TypingWf]
wf_case_branch_context_gen [lemma, in MetaRocq.Template.TypingWf]
wf_inds [lemma, in MetaRocq.Template.TypingWf]
wf_case_predicate_context [lemma, in MetaRocq.Template.TypingWf]
wf_extended_subst [lemma, in MetaRocq.Template.TypingWf]
wf_subst_instance_context [lemma, in MetaRocq.Template.TypingWf]
wf_lift_context [lemma, in MetaRocq.Template.TypingWf]
wf_map2_set_binder_name [lemma, in MetaRocq.Template.TypingWf]
wf_reln [lemma, in MetaRocq.Template.TypingWf]
wf_smash_context [lemma, in MetaRocq.Template.TypingWf]
wf_subst_context [lemma, in MetaRocq.Template.TypingWf]
wf_it_mkProd_or_LetIn [lemma, in MetaRocq.Template.TypingWf]
wf_decl_extends [lemma, in MetaRocq.Template.TypingWf]
wf_extends [lemma, in MetaRocq.Template.TypingWf]
wf_mkApps [lemma, in MetaRocq.Erasure.EInlineProjections]
wf_optimize [lemma, in MetaRocq.Erasure.EInlineProjections]
wf_redp_subterm [instance, in MetaRocq.SafeChecker.PCUICWfReduction]
wf_redp_subterm_rel [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
wf_hnf_subterm [instance, in MetaRocq.SafeChecker.PCUICWfReduction]
wf_hnf_subterm_rel [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
wf_cofixpoint_spine [lemma, in MetaRocq.PCUIC.PCUICClassification]
wf_fixpoint_spine [lemma, in MetaRocq.PCUIC.PCUICClassification]
wf_cofixpoint_inv [lemma, in MetaRocq.PCUIC.PCUICClassification]
wf_fixpoint_inv [lemma, in MetaRocq.PCUIC.PCUICClassification]
wf_sort_super [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_sort_type1 [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_global_ext [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_sort_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_universe_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk_wf [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_glob_debox [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wf_glob_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Wf_size_lt [instance, in MetaRocq.Erasure.EInduction]
wf_branch_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pcontext [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pars [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchesP [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchesb [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branches [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branches_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchP [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchb [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branch [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branch_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicateP [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicateb [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_types [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_ctx_universes_closed [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_closedu [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_make [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_closed [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_closed [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_closed [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level_closed [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_extended_subst [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_projs [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_ctx_universes [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_decl_universes [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_abstract_instance [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_local_ctx_nth_error [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_local_ctx_smash [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_mkApps [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_inds [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_weaken [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_weaken_full [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_inst [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_subst [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_lift [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universeb_instance_forall [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_reflect [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sortb [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_reflect [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universeb [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_subst_instance [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_In [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_sub [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level_sub [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level_mono [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_instantiate [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_subst_instance_sort [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_subst_instance_univ [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instanceP [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_levelP [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instanceb [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_levelb [definition, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_product [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_sup [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_super [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_type1 [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_type0 [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_iff [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
wf_sort_iff [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
wf_universe_iff [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
wf_local_app_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
wf_ind_arities [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_expand_lets_ctx [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_expand_lets [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_trans_env [instance, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_it_mkProd_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_wf_decl_pred [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_global_decl [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_fresh_globals [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_local_closed_context [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
wf_context_sorts [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
wf_cons_inv [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
wf_local_expand_lets0 [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
wf_env_init [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_fresh [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_fresh_globals [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_eta [lemma, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext_map_repr [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext_map [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext_reference [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext [record, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_map_repr [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_map [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_reference [projection, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env [record, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf.efl [variable, in MetaRocq.Erasure.EWellformed]
wf.Σ [variable, in MetaRocq.Erasure.EWellformed]
wfΣ [lemma, in MetaRocq.Erasure.Typed.TypeAnnotations]
wGraph [module, in MetaRocq.Common.uGraph]
wGraph [library]
whne [inductive, in MetaRocq.PCUIC.PCUICNormal]
whne [inductive, in MetaRocq.Template.Normal]
whne_eq_term_upto_univ_napp [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_pres [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_pres1 [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.P [variable, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.Γ [variable, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.Σ [variable, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.flags [variable, in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind [section, in MetaRocq.PCUIC.PCUICNormal]
whne_isConstruct_app [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_dec [definition, in MetaRocq.PCUIC.PCUICNormal]
whne_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_mkApps [lemma, in MetaRocq.PCUIC.PCUICNormal]
whne_sind [definition, in MetaRocq.PCUIC.PCUICNormal]
whne_rec [definition, in MetaRocq.PCUIC.PCUICNormal]
whne_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
whne_rect [definition, in MetaRocq.PCUIC.PCUICNormal]
whne_proj_noiota [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_proj [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_case_noiota [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_case [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_fix_nofix [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_fixapp [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_app [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_const_nodelta [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_const [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_letin_nozeta [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_evar [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_var [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_lam_nobeta [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_rel_nozeta [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_rel [constructor, in MetaRocq.PCUIC.PCUICNormal]
whne_conv_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
whne_All2_fold [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
whne_sind [definition, in MetaRocq.Template.Normal]
whne_ind [definition, in MetaRocq.Template.Normal]
whne_proj [constructor, in MetaRocq.Template.Normal]
whne_case [constructor, in MetaRocq.Template.Normal]
whne_app [constructor, in MetaRocq.Template.Normal]
whne_const [constructor, in MetaRocq.Template.Normal]
whne_evar [constructor, in MetaRocq.Template.Normal]
whne_var [constructor, in MetaRocq.Template.Normal]
whne_rel [constructor, in MetaRocq.Template.Normal]
whnf [inductive, in MetaRocq.PCUIC.PCUICNormal]
whnf [inductive, in MetaRocq.Template.Normal]
whnf_eq_term [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_eq_term_upto_univ_napp [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_isApp [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red1_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_trans [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_refl [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_refl_whne [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps_r_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps_l_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_red [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_sind [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_rec [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_rect [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tPrim [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tCoFix [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tInd [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tConstruct [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tLambda [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tProd [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tSort [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tProj [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tCase [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tFix [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tApp [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tConst [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tEvar [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tVar [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red_tRel [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_red [inductive, in MetaRocq.PCUIC.PCUICNormal]
whnf_pres [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_pres1 [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_tLambda_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_tProd_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_tSort_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_dec [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_whne_dec [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_whne_nodelta_upgrade [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_fixapp' [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps [lemma, in MetaRocq.PCUIC.PCUICNormal]
whnf_sind [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_rec [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_ind [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_rect [definition, in MetaRocq.PCUIC.PCUICNormal]
whnf_prim [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_cofixapp [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_fixapp [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_indapp [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_cstrapp [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_lam [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_prod [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_sort [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_ne [constructor, in MetaRocq.PCUIC.PCUICNormal]
whnf_proj_arg_whne [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_case_arg_whne [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_fix_arg_whne [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_non_cofix_ind_typed [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_finite_ind_typed [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_conv_context [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
whnf_All2_fold [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
whnf_sind [definition, in MetaRocq.Template.Normal]
whnf_ind [definition, in MetaRocq.Template.Normal]
whnf_cofix [constructor, in MetaRocq.Template.Normal]
whnf_fix [constructor, in MetaRocq.Template.Normal]
whnf_indapp [constructor, in MetaRocq.Template.Normal]
whnf_cstrapp [constructor, in MetaRocq.Template.Normal]
whnf_lam [constructor, in MetaRocq.Template.Normal]
whnf_prod [constructor, in MetaRocq.Template.Normal]
whnf_sort [constructor, in MetaRocq.Template.Normal]
whnf_ne [constructor, in MetaRocq.Template.Normal]
whnf_progress [lemma, in MetaRocq.PCUIC.PCUICProgress]
whnf_classification [lemma, in MetaRocq.PCUIC.PCUICClassification]
whnf_classification' [lemma, in MetaRocq.PCUIC.PCUICClassification]
whnf_red_isIndConstructApp [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
whnf_mkApps_tPrim_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
wh_normalization [lemma, in MetaRocq.PCUIC.PCUICNormalization]
wh_neutral_empty [lemma, in MetaRocq.PCUIC.PCUICClassification]
wh_neutral_empty_gen [lemma, in MetaRocq.PCUIC.PCUICClassification]
wh_normal [abbreviation, in MetaRocq.PCUIC.PCUICClassification]
wh_neutral [abbreviation, in MetaRocq.PCUIC.PCUICClassification]
WithCheckerFlags [section, in MetaRocq.PCUIC.PCUICCasesHelper]
WithCheckerFlags.cf [variable, in MetaRocq.PCUIC.PCUICCasesHelper]
WithTemplate [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.is_only_type [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.is_type [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.is_set [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Level [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.is_empty_prefix_with [lemma, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.prefix_with [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.prefix_with_Ok [lemma, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.Raw [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.Raw.prefix_with [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Level.prefix_with [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.nonEmptyLevelExprSet [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.nonEmptyLevelExprSet.prefix_with [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Sort [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Sort.prefix_with [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Universe [module, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmExtractBaseModPathFromMod [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmObj_magic [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmQuoteConstantUniversesAndRelevance [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmQuoteInductiveUniverses [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmQuoteToGlobalReference [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRelaxOnlyType [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRelaxSet [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRelaxSortsM [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetype [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeAroundMetaRocqBug853 [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeMagicRelaxOnlyType [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeMagicRelaxSetInCodomain [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeRelaxOnlyType [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeRelaxSetInCodomain [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmUnfoldQed [definition, in MetaRocq.Quotation.CommonUtils]
WithTemplate.transparentify [abbreviation, in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.U [variable, in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.in_domain [variable, in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.M_monad [variable, in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.M [variable, in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad [section, in MetaRocq.Quotation.CommonUtils]
with_monad.map_branch.bbodyf [variable, in MetaRocq.Template.MonadAst]
with_monad.map_branch.term' [variable, in MetaRocq.Template.MonadAst]
with_monad.map_branch.term [variable, in MetaRocq.Template.MonadAst]
with_monad.map_branch [section, in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k.f [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k.uf [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k.term [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k [section, in MetaRocq.Template.MonadAst]
with_monad.map_predicate.preturnf [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate.paramf [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate.uf [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate.term' [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate.term [variable, in MetaRocq.Template.MonadAst]
with_monad.map_predicate [section, in MetaRocq.Template.MonadAst]
with_monad.M [variable, in MetaRocq.Template.MonadAst]
with_monad.T [variable, in MetaRocq.Template.MonadAst]
with_monad [section, in MetaRocq.Template.MonadAst]
with_monad.map_branch.bcontextf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch.bbodyf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch.term' [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch.term [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch [section, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k.f [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k.uf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k.term [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k [section, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.pcontextf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.preturnf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.paramf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.uf [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.term' [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.term [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate [section, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.M [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.T [variable, in MetaRocq.PCUIC.PCUICMonadAst]
with_monad [section, in MetaRocq.PCUIC.PCUICMonadAst]
with_tc.with_helper.tmEval [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.with_helper.TransLookup_lookup_inductive' [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.with_helper [section, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers.tmFail [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers.tmQuoteInductive [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers.monad_trans [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers [section, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.M [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.T [variable, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc [section, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_listable.FinitelyListable_T [variable, in MetaRocq.Utils.MRListable]
with_listable.Listable_T [variable, in MetaRocq.Utils.MRListable]
with_listable.T [variable, in MetaRocq.Utils.MRListable]
with_listable [section, in MetaRocq.Utils.MRListable]
with_constructor_as_block [projection, in MetaRocq.Erasure.EWcbvEval]
with_guarded_fix [projection, in MetaRocq.Erasure.EWcbvEval]
with_prop_case [projection, in MetaRocq.Erasure.EWcbvEval]
with_monad.Contexts.term'' [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.Contexts.term' [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.Contexts.term [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.Contexts [section, in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap.f [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap.term' [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap.term [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap [section, in MetaRocq.Common.MonadBasicAst]
with_monad.M [variable, in MetaRocq.Common.MonadBasicAst]
with_monad.T [variable, in MetaRocq.Common.MonadBasicAst]
with_monad [section, in MetaRocq.Common.MonadBasicAst]
wrap_error [definition, in MetaRocq.SafeChecker.PCUICErrors]
wrap_error [definition, in MetaRocq.Template.Checker]
ws_wcbv_standardization_fst [lemma, in MetaRocq.PCUIC.PCUICNormalization]
ws_wcbv_standardization [lemma, in MetaRocq.PCUIC.PCUICNormalization]
ws_empty [definition, in MetaRocq.PCUIC.PCUICNormalization]
ws_cumul_pb_terms_refl [lemma, in MetaRocq.PCUIC.PCUICSR]
ws_cumul_pb_terms_eq_trans [lemma, in MetaRocq.PCUIC.PCUICSR]
ws_cumul_pb_eq_trans [lemma, in MetaRocq.PCUIC.PCUICSR]
ws_cumul_pb_meta_refl [lemma, in MetaRocq.PCUIC.PCUICSR]
ws_cumul_ctx_pb_rel_trans [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_ws_cumul_ctx [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_length [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_ws_cumul_ctx [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_smash [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_conv_extended_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_eq_le [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_le_le [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_le_le [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel'_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_zippx [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
ws_cumul_ctx_pb_refl [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_forget [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_sym [instance, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_inv [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_left [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_right [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_trans [instance, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_inv [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_cumul_pb_decls [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_right [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_left [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_decl [abbreviation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt_closed [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_trans [instance, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_conv [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_cumul [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_right [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_left [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_closed_context [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_sym [instance, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl' [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_sind [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_rec [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_ind [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_rect [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_red_r [constructor, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_red_l [constructor, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_compare [constructor, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb [inductive, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_app_same [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_refl [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_true_forget [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_false_forget [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_trans [instance, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_decls_ws_cumul_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_le [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_red [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_context_upto [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context_inv [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
ws_red_confluence [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_pred [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_curry_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_refl_irrel [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_irrel [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_red_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_red_ctx_aux [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_ctx_length [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_ctx_trans [instance, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_ctx_refl [instance, in MetaRocq.PCUIC.PCUICConfluence]
ws_pair_eq_ctx [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_term_eq [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_ctx [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_red_ctx [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_red1_ctx [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_diamond [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_red [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_ws_pred_curry [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red1_pred1 [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_red1_pred1_curry [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_curry [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1 [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_curry [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pair_term [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pair_context [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_pair [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_red [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_red1 [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_context_on_free_vars_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_context_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_context_on_free_vars [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_context_proj' [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_context_proj [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_context [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_term_xpredT [lemma, in MetaRocq.PCUIC.PCUICConfluence]
ws_term_prop [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_term_proj [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_term [definition, in MetaRocq.PCUIC.PCUICConfluence]
ws_cumul_pb_it_mkProd_or_LetIn_smash [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_pb_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_ctx_pb_wf_local [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_inst_variance [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_Prod_Prod_inv_l [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_subst [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_inv [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_eq [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_terms_confl [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_tRel [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_ctx_pb_rel_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_Prim [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Construct [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Evar [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_weaken [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_conv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_ws_cumul_ctx [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_alt [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_rel_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_rel_app [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_rel [definition, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_elim [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_substs_red [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_ty [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_tm [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps_weak [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn_codom [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn_codom [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_bo [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_r [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_l [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_eq_le_gen [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_CoFix [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Fix [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_or_cofix [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_bodies [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_body [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_types [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_type [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_brs [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_one_brs [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_c [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_p [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_App [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Proj_c [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_App_r [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_App_l [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_brs [definition, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_predicate [definition, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Axiom_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Axiom_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_right [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_left [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_red_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_red_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Prod_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_r_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_l_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Sort_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_Prod_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_inv [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l [lemma, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_sym [instance, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_trans [instance, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_Proper [instance, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms [abbreviation, in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_app [lemma, in MetaRocq.PCUIC.PCUICArities]
ws_cumul_ctx_pb_vass [lemma, in MetaRocq.PCUIC.PCUICArities]
ws_cumul_pb_LetIn_l_inv_alt [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
ws_cumul_ctx_pb_rel_cons [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
wt [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
WtContextConversion [section, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
WtContextConversion.cf [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
WtContextConversion.wfΣ [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
WtContextConversion.Σ [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wtcumul [section, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtcumul [section, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wtcumul' [section, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtcumul'.cf [variable, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
_ ;;; _ | _ |-- _ <=[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtcumul.cf [variable, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
_ ;;; _ |-- _ <=[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
_ ;;; _ |-- _ <= _ (type_scope) [notation, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wterm [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
wth [projection, in MetaRocq.SafeChecker.PCUICSafeConversion]
wtp [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
wtsub [section, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub [section, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wtsub.cf [variable, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.cf [variable, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wtsub.wfΣ [variable, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.wfΣ [variable, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wtsub.Σ [variable, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.Σ [variable, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_template_program_fresh [lemma, in MetaRocq.Template.TemplateProgram]
wt_template_program_env [definition, in MetaRocq.Template.TemplateProgram]
wt_template_program [definition, in MetaRocq.Template.TemplateProgram]
wt_closed_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
wt_terms_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICSR]
wt_cumul_pb_refl [lemma, in MetaRocq.PCUIC.PCUICSR]
wt_cumul_pb_equalityP [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_red_r [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_red_l [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_refl [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
wt_conv_conv [definition, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_cum [definition, in MetaRocq.PCUIC.PCUICSubstitution]
wt_conv [definition, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul [definition, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_pb_eq [projection, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_pb_codom [projection, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_pb_dom [projection, in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_pb [record, in MetaRocq.PCUIC.PCUICSubstitution]
wt_pcuic_program [definition, in MetaRocq.PCUIC.PCUICProgram]
wt_ws_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb_forget [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_decl [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_conv_context [abbreviation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_context [abbreviation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_sind [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_rec [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_ind [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_rect [definition, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_vdef [constructor, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_vass [constructor, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls [inductive, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_trans [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cum_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wt_cum_ws_cumul_pb [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wt_closed [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_subst_instance [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_convSpec_convAlgo [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_conv_hetero [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_hetero [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_sind [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_rec [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_ind [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_rect [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_r' [constructor, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_l' [constructor, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_refl' [constructor, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero [inductive, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ctx_rel [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ctx [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_conv [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_sind [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_rec [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ind [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_rect [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_r [constructor, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_l [constructor, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_refl [constructor, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb [inductive, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_codom [projection, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_dom [projection, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_red1 [projection, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1 [record, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_wt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_subterm [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_wf_local [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_ind_app_variance [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
wt_cstrs [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
wt_indices [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wt_terms [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
wt_closed_red_refl [lemma, in MetaRocq.PCUIC.PCUICClassification]
wt_zip_mkapps [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
wt_brs [abbreviation, in MetaRocq.SafeChecker.PCUICTypeChecker]
wt_decl [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
wt_cumul_sind [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_rec [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_ind [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_rect [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_red_r [constructor, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_red_l [constructor, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_refl [constructor, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul [inductive, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_red1_codom [projection, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_red1_dom [projection, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_red1_red1 [projection, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_red1 [record, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_inv [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_subterm [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt'_erase_pcuic_program [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
| 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) |