| 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) |
M (variable)
MakeGraph.ctrs [in MetaRocq.Common.uGraph]MakeGraph.G [in MetaRocq.Common.uGraph]
MakeGraph.Huctx [in MetaRocq.Common.uGraph]
MakeGraph.uctx [in MetaRocq.Common.uGraph]
make_All_All.f [in MetaRocq.Utils.All_Forall]
make_All_All.C [in MetaRocq.Utils.All_Forall]
make_All_All.B [in MetaRocq.Utils.All_Forall]
make_All_All.A [in MetaRocq.Utils.All_Forall]
make_All.f [in MetaRocq.Utils.All_Forall]
make_All.B [in MetaRocq.Utils.All_Forall]
make_All.A [in MetaRocq.Utils.All_Forall]
MapInP.A [in MetaRocq.Utils.MRList]
MapInP.A [in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.B [in MetaRocq.Utils.MRList]
MapInP.B [in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.f [in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.P [in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapOpt.A [in MetaRocq.Utils.monad_utils]
MapOpt.B [in MetaRocq.Utils.monad_utils]
MapOpt.f [in MetaRocq.Utils.monad_utils]
map_onPrim.ont [in MetaRocq.PCUIC.PCUICEtaExpand]
map_onPrim.P' [in MetaRocq.PCUIC.PCUICEtaExpand]
map_onPrim.P [in MetaRocq.PCUIC.PCUICEtaExpand]
map_All.ont [in MetaRocq.PCUIC.PCUICEtaExpand]
map_All.P' [in MetaRocq.PCUIC.PCUICEtaExpand]
map_All.P [in MetaRocq.PCUIC.PCUICEtaExpand]
map_branch_shift.f [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.fn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.T [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.f [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.finst [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.fn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.T [in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_k.g [in MetaRocq.PCUIC.PCUICAst]
map_branch_k.f [in MetaRocq.PCUIC.PCUICAst]
map_branch_k.term' [in MetaRocq.PCUIC.PCUICAst]
map_branch_k.term [in MetaRocq.PCUIC.PCUICAst]
map_branch.g [in MetaRocq.PCUIC.PCUICAst]
map_branch.f [in MetaRocq.PCUIC.PCUICAst]
map_branch.term' [in MetaRocq.PCUIC.PCUICAst]
map_branch.term [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k.f [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k.uf [in MetaRocq.PCUIC.PCUICAst]
map_predicate_k.term [in MetaRocq.PCUIC.PCUICAst]
map_predicate.pcontextf [in MetaRocq.PCUIC.PCUICAst]
map_predicate.preturnf [in MetaRocq.PCUIC.PCUICAst]
map_predicate.paramf [in MetaRocq.PCUIC.PCUICAst]
map_predicate.uf [in MetaRocq.PCUIC.PCUICAst]
map_predicate.term' [in MetaRocq.PCUIC.PCUICAst]
map_predicate.term [in MetaRocq.PCUIC.PCUICAst]
map_All2.f [in MetaRocq.Utils.All_Forall]
map_All2.Q [in MetaRocq.Utils.All_Forall]
map_All2.P [in MetaRocq.Utils.All_Forall]
map_All2.B [in MetaRocq.Utils.All_Forall]
map_All2.A [in MetaRocq.Utils.All_Forall]
map_All.fn [in MetaRocq.Utils.All_Forall]
map_All.P [in MetaRocq.Utils.All_Forall]
map_All.Q [in MetaRocq.Utils.All_Forall]
map_All.C [in MetaRocq.Utils.All_Forall]
map_All.B [in MetaRocq.Utils.All_Forall]
map_All.A [in MetaRocq.Utils.All_Forall]
map_branch.bbodyf [in MetaRocq.Template.Ast]
map_branch.term' [in MetaRocq.Template.Ast]
map_branch.term [in MetaRocq.Template.Ast]
map_predicate_k.f [in MetaRocq.Template.Ast]
map_predicate_k.uf [in MetaRocq.Template.Ast]
map_predicate_k.term [in MetaRocq.Template.Ast]
map_predicate.preturnf [in MetaRocq.Template.Ast]
map_predicate.paramf [in MetaRocq.Template.Ast]
map_predicate.uf [in MetaRocq.Template.Ast]
map_predicate.term' [in MetaRocq.Template.Ast]
map_predicate.term [in MetaRocq.Template.Ast]
map_All2_dep.F [in MetaRocq.Erasure.EPrimitive]
map_All2_dep.hP [in MetaRocq.Erasure.EPrimitive]
map_All2_dep.P [in MetaRocq.Erasure.EPrimitive]
map_All2_dep.B [in MetaRocq.Erasure.EPrimitive]
map_All2_dep.A [in MetaRocq.Erasure.EPrimitive]
Map2Bias.A [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.B [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.C [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.default [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.f [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2.A [in MetaRocq.Utils.MRList]
map2.B [in MetaRocq.Utils.MRList]
map2.C [in MetaRocq.Utils.MRList]
map2.f [in MetaRocq.Utils.MRList]
Measure.cf [in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.flags [in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.no [in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.Σ [in MetaRocq.SafeChecker.PCUICSafeReduce]
MkAppsInd.MkApps_case.pforce [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.plazy [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pprim [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pcofix [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pfix [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pproj [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pcase [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pconstruct [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pconst [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.papp [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.plet [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.plam [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pevar [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pvar [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.prel [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pbox [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.P [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pforce [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.plazy [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pprim [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pcofix [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pfix [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pproj [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pcase [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pconstruct [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pconst [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.papp [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.plet [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.plam [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pevar [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pvar [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.prel [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pbox [in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.P [in MetaRocq.Erasure.EInduction]
MonadAllAll.A [in MetaRocq.Utils.monad_utils]
MonadAllAll.f [in MetaRocq.Utils.monad_utils]
MonadAllAll.M [in MetaRocq.Utils.monad_utils]
MonadAllAll.P [in MetaRocq.Utils.monad_utils]
MonadAllAll.Q [in MetaRocq.Utils.monad_utils]
MonadAllAll.T [in MetaRocq.Utils.monad_utils]
MonadOperations.A [in MetaRocq.Utils.monad_utils]
MonadOperations.A [in MetaRocq.Utils.monad_utils]
MonadOperations.B [in MetaRocq.Utils.monad_utils]
MonadOperations.B [in MetaRocq.Utils.monad_utils]
MonadOperations.C [in MetaRocq.Utils.monad_utils]
MonadOperations.e [in MetaRocq.Utils.monad_utils]
MonadOperations.E [in MetaRocq.Utils.monad_utils]
MonadOperations.f [in MetaRocq.Utils.monad_utils]
MonadOperations.f [in MetaRocq.Utils.monad_utils]
MonadOperations.g [in MetaRocq.Utils.monad_utils]
MonadOperations.h [in MetaRocq.Utils.monad_utils]
MonadOperations.M [in MetaRocq.Utils.monad_utils]
MonadOperations.M [in MetaRocq.Utils.monad_utils]
MonadOperations.ME [in MetaRocq.Utils.monad_utils]
MonadOperations.T [in MetaRocq.Utils.monad_utils]
MonadOperations.T [in MetaRocq.Utils.monad_utils]
monad_Alli_nth.P [in MetaRocq.Utils.monad_utils]
monad_Alli_nth.A [in MetaRocq.Utils.monad_utils]
monad_Alli_nth.M [in MetaRocq.Utils.monad_utils]
monad_Alli_nth.T [in MetaRocq.Utils.monad_utils]
MoreCongruenceLemmas.cf [in MetaRocq.PCUIC.PCUICConversion]
MoreCongruenceLemmas.wfΣ [in MetaRocq.PCUIC.PCUICConversion]
MoreCongruenceLemmas.Σ [in MetaRocq.PCUIC.PCUICConversion]
| 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) |