| 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 (definition)
wcbv_red1_sind [in MetaRocq.PCUIC.PCUICWcbvEval]wcbv_red1_rec [in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_ind [in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_rect [in MetaRocq.PCUIC.PCUICWcbvEval]
wcored [in MetaRocq.SafeChecker.PCUICSafeConversion]
weakening_on_global_decl [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_prop_strictly_on_decls_to_strictly_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_decls_to_strictly_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_to_strictly_on_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_to_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_strictly_on_decls_to_strictly_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_decls_to_strictly_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_to_strictly_on_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_to_decls [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_on_decls_prop [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_decls_prop [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_decls_prop [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_on_decls_prop_full [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_strictly_decls_prop_full [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_decls_prop_full [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_gen [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full_gen [in MetaRocq.PCUIC.PCUICWeakeningEnv]
WeightedGraph.acyclic_no_sloop [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop' [in MetaRocq.Utils.wGraph]
WeightedGraph.add_end [in MetaRocq.Utils.wGraph]
WeightedGraph.add_edge [in MetaRocq.Utils.wGraph]
WeightedGraph.add_node [in MetaRocq.Utils.wGraph]
WeightedGraph.concat [in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling [in MetaRocq.Utils.wGraph]
WeightedGraph.diff [in MetaRocq.Utils.wGraph]
WeightedGraph.Disjoint [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd [in MetaRocq.Utils.wGraph]
WeightedGraph.E [in MetaRocq.Utils.wGraph]
WeightedGraph.EdgeOf [in MetaRocq.Utils.wGraph]
WeightedGraph.edge_map [in MetaRocq.Utils.wGraph]
WeightedGraph.edge_pathOf [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.compare [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.compare_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eqb [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq_leibniz [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq_dec [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.eq_equiv [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.lt [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.lt_compat [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.lt_strorder [in MetaRocq.Utils.wGraph]
WeightedGraph.Edge.t [in MetaRocq.Utils.wGraph]
WeightedGraph.e_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.e_target [in MetaRocq.Utils.wGraph]
WeightedGraph.e_source [in MetaRocq.Utils.wGraph]
WeightedGraph.first_in [in MetaRocq.Utils.wGraph]
WeightedGraph.from_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.from_G'_path [in MetaRocq.Utils.wGraph]
WeightedGraph.from1 [in MetaRocq.Utils.wGraph]
WeightedGraph.from2 [in MetaRocq.Utils.wGraph]
WeightedGraph.G' [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension [in MetaRocq.Utils.wGraph]
WeightedGraph.is_acyclic [in MetaRocq.Utils.wGraph]
WeightedGraph.is_nonpos [in MetaRocq.Utils.wGraph]
WeightedGraph.is_simple [in MetaRocq.Utils.wGraph]
WeightedGraph.labelling [in MetaRocq.Utils.wGraph]
WeightedGraph.length [in MetaRocq.Utils.wGraph]
WeightedGraph.leqb_vertices [in MetaRocq.Utils.wGraph]
WeightedGraph.leq_vertices [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_map_path2 [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_fast [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0 [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_sub [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp00 [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp00_fast [in MetaRocq.Utils.wGraph]
WeightedGraph.map_spath [in MetaRocq.Utils.wGraph]
WeightedGraph.map_path [in MetaRocq.Utils.wGraph]
WeightedGraph.nodes [in MetaRocq.Utils.wGraph]
WeightedGraph.opp_edge [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_add_end [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_sind [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_rec [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_ind [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_rect [in MetaRocq.Utils.wGraph]
WeightedGraph.PosPathOf [in MetaRocq.Utils.wGraph]
WeightedGraph.reduce [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l' [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.r [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.stdl [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_map [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_path [in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux [in MetaRocq.Utils.wGraph]
WeightedGraph.s [in MetaRocq.Utils.wGraph]
WeightedGraph.sconcat [in MetaRocq.Utils.wGraph]
WeightedGraph.simplify [in MetaRocq.Utils.wGraph]
WeightedGraph.simplify2 [in MetaRocq.Utils.wGraph]
WeightedGraph.simplify2' [in MetaRocq.Utils.wGraph]
WeightedGraph.snodes [in MetaRocq.Utils.wGraph]
WeightedGraph.snodes_Subset [in MetaRocq.Utils.wGraph]
WeightedGraph.spath_one [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_sub [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_sind [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_rec [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_ind [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_rect [in MetaRocq.Utils.wGraph]
WeightedGraph.split [in MetaRocq.Utils.wGraph]
WeightedGraph.split' [in MetaRocq.Utils.wGraph]
WeightedGraph.sto_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph_on_edge [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.G' [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.sto_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.to_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.succs [in MetaRocq.Utils.wGraph]
WeightedGraph.sweight [in MetaRocq.Utils.wGraph]
WeightedGraph.t [in MetaRocq.Utils.wGraph]
WeightedGraph.to_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.to_label [in MetaRocq.Utils.wGraph]
WeightedGraph.to_simple [in MetaRocq.Utils.wGraph]
WeightedGraph.to_pathOf [in MetaRocq.Utils.wGraph]
WeightedGraph.V [in MetaRocq.Utils.wGraph]
WeightedGraph.weight [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_spath2 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_spath1 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_path2 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_map_path1 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_SPath_sub [in MetaRocq.Utils.wGraph]
wellformed [in MetaRocq.Erasure.ErasureProperties]
wellformed [in MetaRocq.Erasure.EWellformed]
wellinferred_sind [in MetaRocq.SafeChecker.PCUICSafeRetyping]
wellinferred_ind [in MetaRocq.SafeChecker.PCUICSafeRetyping]
welltyped_sind [in MetaRocq.PCUIC.PCUICTyping]
welltyped_ind [in MetaRocq.PCUIC.PCUICTyping]
well_typed [in MetaRocq.Erasure.Prelim]
well_prop_sind [in MetaRocq.Examples.tauto]
well_prop_rec [in MetaRocq.Examples.tauto]
well_prop_ind [in MetaRocq.Examples.tauto]
well_prop_rect [in MetaRocq.Examples.tauto]
well_subst_closed_subst [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
well_subst_usubst [in MetaRocq.PCUIC.Typing.PCUICInstTyp]
well_sorted [in MetaRocq.SafeChecker.PCUICSafeRetyping]
well_subst [in MetaRocq.PCUIC.Syntax.PCUICInstDef]
weqt [in MetaRocq.SafeChecker.PCUICSafeConversion]
wf [in MetaRocq.PCUIC.PCUICTyping]
wf [in MetaRocq.Template.Typing]
wfterm [in MetaRocq.Template.TemplateCheckWf]
wf_reduction_aux [in MetaRocq.Erasure.ErasureFunction]
wf_ext [in MetaRocq.PCUIC.PCUICTyping]
wf_cofixpoint [in MetaRocq.PCUIC.PCUICTyping]
wf_cofixpoint_gen [in MetaRocq.PCUIC.PCUICTyping]
wf_fixpoint [in MetaRocq.PCUIC.PCUICTyping]
wf_fixpoint_gen [in MetaRocq.PCUIC.PCUICTyping]
wf_brs [in MetaRocq.Erasure.ErasureProperties]
wf_ext_global_uctx_invariants [in MetaRocq.PCUIC.PCUICGlobalEnv]
wf_global_uctx_invariants [in MetaRocq.PCUIC.PCUICGlobalEnv]
wf_fixpoints [in MetaRocq.Erasure.ErasureFunctionProperties]
wf_decl_pred [in MetaRocq.Template.WfAst]
wf_decl [in MetaRocq.Template.WfAst]
wf_Inv [in MetaRocq.Template.WfAst]
wf_sind [in MetaRocq.Template.WfAst]
wf_rec [in MetaRocq.Template.WfAst]
wf_ind [in MetaRocq.Template.WfAst]
wf_rect [in MetaRocq.Template.WfAst]
wf_typing_spine [in MetaRocq.PCUIC.PCUICArities]
wf_eprogram_env [in MetaRocq.Erasure.EProgram]
wf_eprogram [in MetaRocq.Erasure.EProgram]
wf_cs_sorts [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ind_types [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_env_check_ws_cumul_ctx [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_env_check_cumul_decl [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_env_conv [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_inductives_mapping [in MetaRocq.Erasure.EReorderCstrs]
wf_inductive_mapping [in MetaRocq.Erasure.EReorderCstrs]
wf_reordering [in MetaRocq.Erasure.EReorderCstrs]
wf_tags_list [in MetaRocq.Erasure.EReorderCstrs]
wf_tags [in MetaRocq.Erasure.EReorderCstrs]
wf_program [in MetaRocq.Template.TemplateCheckWf]
wf_global_env [in MetaRocq.Template.TemplateCheckWf]
wf_global_declarations [in MetaRocq.Template.TemplateCheckWf]
wf_global_decl [in MetaRocq.Template.TemplateCheckWf]
wf_ext_wf [in MetaRocq.Template.Typing]
wf_ext [in MetaRocq.Template.Typing]
wf_cofixpoint [in MetaRocq.Template.Typing]
wf_fixpoint [in MetaRocq.Template.Typing]
wf_template_inductives_mapping [in MetaRocq.ErasurePlugin.Erasure]
wf_template_inductive_mapping [in MetaRocq.ErasurePlugin.Erasure]
wf_pcuic_inductives_mapping [in MetaRocq.ErasurePlugin.Erasure]
wf_pcuic_inductive_mapping [in MetaRocq.ErasurePlugin.Erasure]
wf_glob_sind [in MetaRocq.Erasure.EWellformed]
wf_glob_ind [in MetaRocq.Erasure.EWellformed]
wf_global_decl [in MetaRocq.Erasure.EWellformed]
wf_minductive [in MetaRocq.Erasure.EWellformed]
wf_inductive [in MetaRocq.Erasure.EWellformed]
wf_projections [in MetaRocq.Erasure.EWellformed]
wf_brs [in MetaRocq.Erasure.EWellformed]
wf_fix_gen [in MetaRocq.Erasure.EWellformed]
wf_redp_subterm_rel [in MetaRocq.SafeChecker.PCUICWfReduction]
wf_hnf_subterm_rel [in MetaRocq.SafeChecker.PCUICWfReduction]
wf_global_ext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_branchesb [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branches [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branches_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchb [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branch [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branch_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicateb [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate_gen [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_ctx_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_decl_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sortb [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universeb [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instanceb [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_levelb [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_iff [in MetaRocq.SafeChecker.PCUICSafeConversion]
wf_sort_iff [in MetaRocq.SafeChecker.PCUICSafeConversion]
wf_universe_iff [in MetaRocq.SafeChecker.PCUICSafeConversion]
wf_global_decl [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_env_init [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
whne_dec [in MetaRocq.PCUIC.PCUICNormal]
whne_sind [in MetaRocq.PCUIC.PCUICNormal]
whne_rec [in MetaRocq.PCUIC.PCUICNormal]
whne_ind [in MetaRocq.PCUIC.PCUICNormal]
whne_rect [in MetaRocq.PCUIC.PCUICNormal]
whne_sind [in MetaRocq.Template.Normal]
whne_ind [in MetaRocq.Template.Normal]
whnf_red_sind [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_rec [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_ind [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_rect [in MetaRocq.PCUIC.PCUICNormal]
whnf_dec [in MetaRocq.PCUIC.PCUICNormal]
whnf_whne_dec [in MetaRocq.PCUIC.PCUICNormal]
whnf_sind [in MetaRocq.PCUIC.PCUICNormal]
whnf_rec [in MetaRocq.PCUIC.PCUICNormal]
whnf_ind [in MetaRocq.PCUIC.PCUICNormal]
whnf_rect [in MetaRocq.PCUIC.PCUICNormal]
whnf_sind [in MetaRocq.Template.Normal]
whnf_ind [in MetaRocq.Template.Normal]
WithTemplate.is_only_type [in MetaRocq.Quotation.CommonUtils]
WithTemplate.is_type [in MetaRocq.Quotation.CommonUtils]
WithTemplate.is_set [in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.prefix_with [in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.Raw.prefix_with [in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Level.prefix_with [in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.nonEmptyLevelExprSet.prefix_with [in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.Sort.prefix_with [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmExtractBaseModPathFromMod [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmObj_magic [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmQuoteConstantUniversesAndRelevance [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmQuoteInductiveUniverses [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmQuoteToGlobalReference [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRelaxOnlyType [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRelaxSet [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRelaxSortsM [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetype [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeAroundMetaRocqBug853 [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeMagicRelaxOnlyType [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeMagicRelaxSetInCodomain [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeRelaxOnlyType [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmRetypeRelaxSetInCodomain [in MetaRocq.Quotation.CommonUtils]
WithTemplate.tmUnfoldQed [in MetaRocq.Quotation.CommonUtils]
wrap_error [in MetaRocq.SafeChecker.PCUICErrors]
wrap_error [in MetaRocq.Template.Checker]
ws_empty [in MetaRocq.PCUIC.PCUICNormalization]
ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_sind [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_rec [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_ind [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_rect [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_pair_eq_ctx [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_ctx [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_ctx [in MetaRocq.PCUIC.PCUICConfluence]
ws_red1_ctx [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_curry [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1 [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_curry [in MetaRocq.PCUIC.PCUICConfluence]
ws_pair_term [in MetaRocq.PCUIC.PCUICConfluence]
ws_pair_context [in MetaRocq.PCUIC.PCUICConfluence]
ws_pair [in MetaRocq.PCUIC.PCUICConfluence]
ws_red [in MetaRocq.PCUIC.PCUICConfluence]
ws_red1 [in MetaRocq.PCUIC.PCUICConfluence]
ws_context_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
ws_context_proj' [in MetaRocq.PCUIC.PCUICConfluence]
ws_context_proj [in MetaRocq.PCUIC.PCUICConfluence]
ws_context [in MetaRocq.PCUIC.PCUICConfluence]
ws_term_prop [in MetaRocq.PCUIC.PCUICConfluence]
ws_term_proj [in MetaRocq.PCUIC.PCUICConfluence]
ws_term [in MetaRocq.PCUIC.PCUICConfluence]
ws_cumul_ctx_pb_rel [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_brs [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_predicate [in MetaRocq.PCUIC.PCUICConversion]
wt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wterm [in MetaRocq.SafeChecker.PCUICSafeConversion]
wt_template_program_env [in MetaRocq.Template.TemplateProgram]
wt_template_program [in MetaRocq.Template.TemplateProgram]
wt_conv_conv [in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul_cum [in MetaRocq.PCUIC.PCUICSubstitution]
wt_conv [in MetaRocq.PCUIC.PCUICSubstitution]
wt_cumul [in MetaRocq.PCUIC.PCUICSubstitution]
wt_pcuic_program [in MetaRocq.PCUIC.PCUICProgram]
wt_decl [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_sind [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_rec [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_ind [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls_rect [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_conv_hetero [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_hetero [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_sind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_rec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_ind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_rect [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ctx_rel [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_conv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_sind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_rec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ind [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_rect [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_subterm [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_indices [in MetaRocq.SafeChecker.PCUICSafeChecker]
wt_terms [in MetaRocq.SafeChecker.PCUICSafeChecker]
wt_decl [in MetaRocq.SafeChecker.PCUICTypeChecker]
wt_cumul_sind [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_rec [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_ind [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_cumul_rect [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt_subterm [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wt'_erase_pcuic_program [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) |