| 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 (variable)
WcbvEnv.efl [in MetaRocq.Erasure.EWcbvEval]WcbvEnv.wfl [in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.F [in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.P [in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.eval [in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.term' [in MetaRocq.Erasure.EWcbvEval]
Wcbv.map_eval_prim.term [in MetaRocq.Erasure.EWcbvEval]
Wcbv.wfl [in MetaRocq.Erasure.EWcbvEval]
Wcbv.wfl [in MetaRocq.Erasure.EWcbvEval]
Wcbv.Σ [in MetaRocq.Template.WcbvEval]
Wcbv.Σ [in MetaRocq.Erasure.EWcbvEval]
Wcbv.Σ [in MetaRocq.Erasure.EWcbvEval]
Wcbv.Σ [in MetaRocq.Erasure.EWcbvEvalNamed]
Wcbv.Σ [in MetaRocq.PCUIC.PCUICWcbvEval]
WeakEtaExp.Σ [in MetaRocq.Erasure.EEtaExpanded]
WeightedGraph.ExtendLabelling.acG2 [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.embed [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.Gl [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.HGl [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.l [in MetaRocq.Utils.wGraph]
WeightedGraph.ExtendLabelling.l' [in MetaRocq.Utils.wGraph]
WeightedGraph.FirstVertexIn.G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.FirstVertexIn.G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.graph.G [in MetaRocq.Utils.wGraph]
WeightedGraph.graph.HI [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.Border.ext [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.Border.G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.bs [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.ext [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath.G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath.G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.MapSPath.on_edge [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.embed [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.Gl [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.HGl [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.l [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelOn.preserves_edges [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.acG [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.d [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.Hk [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.Hl [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.k [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.l [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling.x [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.G [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.invG [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.hx [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.hxy [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.hy [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.nxy [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.x [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs.y [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.G [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.HG [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.HI [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.Hxs [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.K [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.Vx [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.Vy [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.x_0 [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph.subgraph2.y_0 [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.G [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.HG [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.HI [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.Hxs [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.K [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.Vx [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.Vy [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.x_0 [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.graph2.y_0 [in MetaRocq.Utils.wGraph]
wellscoped.Def.Σ [in MetaRocq.Erasure.ErasureProperties]
WfAst.cf [in MetaRocq.Template.TypingWf]
WfAst.Σ [in MetaRocq.Template.TypingWf]
WfEnv.cf [in MetaRocq.PCUIC.PCUICSpine]
WfEnv.cf [in MetaRocq.PCUIC.PCUICSpine]
WfEnv.cf [in MetaRocq.PCUIC.PCUICArities]
WfEnv.cf [in MetaRocq.PCUIC.PCUICContexts]
WfEnv.cf [in MetaRocq.PCUIC.PCUICProgress]
WfEnv.cf [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
WfEnv.guard [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
WfEnv.wfΣ [in MetaRocq.PCUIC.PCUICSpine]
WfEnv.wfΣ [in MetaRocq.PCUIC.PCUICSpine]
WfEnv.wfΣ [in MetaRocq.PCUIC.PCUICArities]
WfEnv.wfΣ [in MetaRocq.PCUIC.PCUICContexts]
WfEnv.wfΣ [in MetaRocq.PCUIC.PCUICProgress]
WfEnv.Σ [in MetaRocq.PCUIC.PCUICSpine]
WfEnv.Σ [in MetaRocq.PCUIC.PCUICSpine]
WfEnv.Σ [in MetaRocq.PCUIC.PCUICArities]
WfEnv.Σ [in MetaRocq.PCUIC.PCUICContexts]
WfEnv.Σ [in MetaRocq.PCUIC.PCUICProgress]
WfLookup.cf [in MetaRocq.Template.TypingWf]
WfLookup.Σ [in MetaRocq.Template.TypingWf]
WfRed.cf [in MetaRocq.Template.TypingWf]
WfRed.Σ [in MetaRocq.Template.TypingWf]
wf.efl [in MetaRocq.Erasure.EWellformed]
wf.Σ [in MetaRocq.Erasure.EWellformed]
whne_red1_ind.P [in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.Γ [in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.Σ [in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind.flags [in MetaRocq.PCUIC.PCUICNormal]
WithCheckerFlags.cf [in MetaRocq.PCUIC.PCUICCasesHelper]
WithTemplate.with_monad.U [in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.in_domain [in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.M_monad [in MetaRocq.Quotation.CommonUtils]
WithTemplate.with_monad.M [in MetaRocq.Quotation.CommonUtils]
with_monad.map_branch.bbodyf [in MetaRocq.Template.MonadAst]
with_monad.map_branch.term' [in MetaRocq.Template.MonadAst]
with_monad.map_branch.term [in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k.f [in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k.uf [in MetaRocq.Template.MonadAst]
with_monad.map_predicate_k.term [in MetaRocq.Template.MonadAst]
with_monad.map_predicate.preturnf [in MetaRocq.Template.MonadAst]
with_monad.map_predicate.paramf [in MetaRocq.Template.MonadAst]
with_monad.map_predicate.uf [in MetaRocq.Template.MonadAst]
with_monad.map_predicate.term' [in MetaRocq.Template.MonadAst]
with_monad.map_predicate.term [in MetaRocq.Template.MonadAst]
with_monad.M [in MetaRocq.Template.MonadAst]
with_monad.T [in MetaRocq.Template.MonadAst]
with_monad.map_branch.bcontextf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch.bbodyf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch.term' [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_branch.term [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k.f [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k.uf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate_k.term [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.pcontextf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.preturnf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.paramf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.uf [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.term' [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.map_predicate.term [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.M [in MetaRocq.PCUIC.PCUICMonadAst]
with_monad.T [in MetaRocq.PCUIC.PCUICMonadAst]
with_tc.with_helper.tmEval [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.with_helper.TransLookup_lookup_inductive' [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers.tmFail [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers.tmQuoteInductive [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.helpers.monad_trans [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.M [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_tc.T [in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
with_listable.FinitelyListable_T [in MetaRocq.Utils.MRListable]
with_listable.Listable_T [in MetaRocq.Utils.MRListable]
with_listable.T [in MetaRocq.Utils.MRListable]
with_monad.Contexts.term'' [in MetaRocq.Common.MonadBasicAst]
with_monad.Contexts.term' [in MetaRocq.Common.MonadBasicAst]
with_monad.Contexts.term [in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap.f [in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap.term' [in MetaRocq.Common.MonadBasicAst]
with_monad.ContextMap.term [in MetaRocq.Common.MonadBasicAst]
with_monad.M [in MetaRocq.Common.MonadBasicAst]
with_monad.T [in MetaRocq.Common.MonadBasicAst]
WtContextConversion.cf [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
WtContextConversion.wfΣ [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
WtContextConversion.Σ [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wtcumul'.cf [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtcumul.cf [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.cf [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.cf [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wtsub.wfΣ [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.wfΣ [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
wtsub.Σ [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wtsub.Σ [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
| 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) |