| 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) |
other
_ ++ _ (bs_scope) [notation, in MetaRocq.Utils.bytestring]_ ,, _ (erasure) [notation, in MetaRocq.Erasure.EAst]
_ { _ := _ } (erasure) [notation, in MetaRocq.Erasure.ELiftSubst]
` _ (metarocq_scope) [notation, in MetaRocq.SafeChecker.PCUICSafeReduce]
! (metarocq_scope) [notation, in MetaRocq.Utils.MRPrelude]
_ .2 (pair_scope) [notation, in MetaRocq.Utils.MRProd]
_ .1 (pair_scope) [notation, in MetaRocq.Utils.MRProd]
_ ⊢ _ ≤[ _ ] _ ✓ (pcuic) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ ≤ _ (pcuic) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ = _ (pcuic) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ ≤[ _ ] _ (pcuic) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ ⇝ _ (pcuic) [notation, in MetaRocq.PCUIC.PCUICContextConversion]
⇑^ _ _ (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ ⋅n _ (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
↑^ _ (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ ∘s _ (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
↑ (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ ⋅ _ (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ .[ _ ] (sigma_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ =2 _ (signature_scope) [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ ^ _ (string_scope2) [notation, in MetaRocq.Utils.utils]
_ ;;; _ |- _ <= _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativity]
_ ;;; _ |- _ = _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativity]
_ ;;; _ |- _ <=[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativity]
_ ;;; _ |- _ ◃ _ (type_scope) [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹{ _ } ( _ , _ ) (type_scope) [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹Π ( _ , _ , _ ) (type_scope) [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹□ _ (type_scope) [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹ _ (type_scope) [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
_ ⊢ _ <==[ _ , _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICEquality]
_ ;;; _ |-[ _ ] _ = _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICSubstitution]
_ ;;; _ |-[ _ ] _ <= _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICSubstitution]
_ ;;; _ |-[ _ ] _ <=[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICSubstitution]
_ ⊢ _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.ErasureCorrectness]
_ |-p _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.ErasureCorrectness]
_ * _ (type_scope2) [notation, in MetaRocq.Utils.utils]
_ ;;; _ ⊢ _ = _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ;;; _ ⊢ _ ≤ _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ;;; _ ⊢ _ ≤[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ p⊢ _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.Typed.ErasureCorrectness]
_ e⊢ _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.Typed.WcbvEvalAux]
_ ⊢ _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.EDeps]
_ p⊢ _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
_ ⊢ _ =s _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
_ ⊢ _ ≤s _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
_ ⊢ _ ≤s[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
_ ;;; _ ⊢ _ ≤s[ _ ] _ (type_scope) [notation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
wf_local _ _ (type_scope) [notation, in MetaRocq.Template.Typing]
_ ;;; _ |- _ : _ (type_scope) [notation, in MetaRocq.Template.Typing]
_ ;;; _ |- _ <= _ (type_scope) [notation, in MetaRocq.Template.Typing]
_ ;;; _ |- _ = _ (type_scope) [notation, in MetaRocq.Template.Typing]
() (type_scope) [notation, in MetaRocq.Template.Checker]
[ × _ , _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ , _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
[ × _ & _ ] (type_scope) [notation, in MetaRocq.Utils.MRProd]
_ ;;; _ |- _ ~~ _ (type_scope) [notation, in MetaRocq.Erasure.EArities]
_ ⊢p _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.EArities]
_ =2 _ (type_scope) [notation, in MetaRocq.Utils.MRPrelude]
_ =1 _ (type_scope) [notation, in MetaRocq.Utils.MRPrelude]
∑ _ .. _ , _ (type_scope) [notation, in MetaRocq.Utils.MRPrelude]
_ ⊢ _ ⇓ _ (type_scope) [notation, in MetaRocq.Erasure.ECoInductiveToInductive]
⟦ _ ⟧_ _ (univ_scope) [notation, in MetaRocq.Common.Universes]
_ ⊢ _ <===[ _ ] _ [notation, in MetaRocq.PCUIC.PCUICCumulativity]
_ ;;; _ ⊢ _ ⇝1 _ [notation, in MetaRocq.PCUIC.PCUICSR]
_ ≡' _ [notation, in MetaRocq.PCUIC.PCUICEquality]
_ ≡ _ [notation, in MetaRocq.PCUIC.PCUICEquality]
_ # _ [notation, in MetaRocq.Utils.MREquality]
_ ?? _ [notation, in MetaRocq.Utils.MRCompare]
_ ;;; _ |- _ = _ ✓ [notation, in MetaRocq.PCUIC.PCUICSubstitution]
_ ;;; _ |- _ <= _ ✓ [notation, in MetaRocq.PCUIC.PCUICSubstitution]
_ @[ _ ] [notation, in MetaRocq.Common.Universes]
_ ⊂?_cs _ [notation, in MetaRocq.Common.Universes]
_ ==_cs _ [notation, in MetaRocq.Common.Universes]
_ ⊂_cs _ [notation, in MetaRocq.Common.Universes]
_ =_cs _ [notation, in MetaRocq.Common.Universes]
_ ==_cset _ [notation, in MetaRocq.Common.Universes]
_ =_cset _ [notation, in MetaRocq.Common.Universes]
_ ==_lset _ [notation, in MetaRocq.Common.Universes]
_ =_lset _ [notation, in MetaRocq.Common.Universes]
_ =kn _ [notation, in MetaRocq.Erasure.ErasureFunction]
_ ;;; _ ⊢ _ ⇝ _ [notation, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
_ ;;; _ |- _ : _ [notation, in MetaRocq.PCUIC.PCUICTyping]
_ ==? _ [notation, in MetaRocq.Common.Reflect]
_ :: _ [notation, in MetaRocq.Utils.MRString]
_ ⊨ _ \ _ by _ ⨷ _ [notation, in MetaRocq.PCUIC.utils.PCUICUtils]
_ ⊗ _ [notation, in MetaRocq.PCUIC.utils.PCUICUtils]
_ ⊩ _ ⨶ _ [notation, in MetaRocq.PCUIC.utils.PCUICUtils]
_ ;;; _ ⊢ _ : _ [notation, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
_ ;;; _ ⊢ _ ⇝1 _ [notation, in MetaRocq.PCUIC.PCUICConversion]
_ ≡Γ _ [notation, in MetaRocq.PCUIC.PCUICAlpha]
_ ≡α _ [notation, in MetaRocq.PCUIC.PCUICAlpha]
_ ∘i _ [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
_ ,,, _ [notation, in MetaRocq.Common.BasicAst]
_ ,, _ [notation, in MetaRocq.Common.BasicAst]
_ ;;; _ |- _ =s _ [notation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
_ ;;; _ |- _ <=s _ [notation, in MetaRocq.PCUIC.PCUICCumulativitySpec]
_ { _ := _ } [notation, in MetaRocq.PCUIC.PCUICAst]
_ ==? _ [notation, in MetaRocq.Template.ReflectAst]
_ ;;; _ |- _ <=[ _ ] _ [notation, in MetaRocq.Template.Typing]
_ ;;; _ |- _ ⇝* _ [notation, in MetaRocq.PCUIC.PCUICReduction]
_ ;;; _ |- _ ⇝ _ [notation, in MetaRocq.PCUIC.PCUICReduction]
_ <~> _ [notation, in MetaRocq.Utils.MRRelations]
_ ∼_ext _ [notation, in MetaRocq.SafeChecker.PCUICWfEnv]
_ ∼ _ [notation, in MetaRocq.SafeChecker.PCUICWfEnv]
_ .p2 [notation, in MetaRocq.Utils.MRProd]
_ .p1 [notation, in MetaRocq.Utils.MRProd]
_ × _ [notation, in MetaRocq.Utils.MRProd]
_ ;;; _ ⊩ _ ~ _ [notation, in MetaRocq.Erasure.EWcbvEvalNamed]
_ ;;; _ |- _ ⇝ℇ _ [notation, in MetaRocq.Erasure.Extract]
_ =_g _ [notation, in MetaRocq.Common.uGraph]
_ =_gcs _ [notation, in MetaRocq.Common.uGraph]
_ .π2 [notation, in MetaRocq.Utils.MRPrelude]
_ .π1 [notation, in MetaRocq.Utils.MRPrelude]
_ ∘ _ [notation, in MetaRocq.Utils.MRPrelude]
_ ⊢ _ ⇝ᵥ _ [notation, in MetaRocq.PCUIC.PCUICWcbvEval]
_ ==? _ [notation, in MetaRocq.PCUIC.Syntax.PCUICReflect]
_ { _ := _ } [notation, in MetaRocq.Template.Ast]
_ == _ [notation, in MetaRocq.Utils.ReflectEq]
eta_compose [notation, in MetaRocq.Utils.MRPrelude]
lens [notation, in MetaRocq.PCUIC.Syntax.PCUICTactics]
precompose [notation, in MetaRocq.Utils.MRRelations]
wf_local_bd_rel _ _ _ [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
wf_local_bd _ _ [notation, in MetaRocq.PCUIC.Bidirectional.BDTyping]
wf_local _ _ [notation, in MetaRocq.PCUIC.PCUICTyping]
__ [notation, in MetaRocq.Template.Lib]
!! _ [notation, in MetaRocq.PCUIC.PCUICInductiveInversion]
#| _ | [notation, in MetaRocq.Utils.MRList]
$name _ [notation, in MetaRocq.Template.Lib]
$quote_def_rec _ [notation, in MetaRocq.Template.Lib]
$quote_def _ [notation, in MetaRocq.Template.Lib]
$quote_rec _ [notation, in MetaRocq.Template.Lib]
$quote _ [notation, in MetaRocq.Template.Lib]
$run _ [notation, in MetaRocq.Template.Lib]
$unquote _ : _ [notation, in MetaRocq.Template.Lib]
$unquote _ [notation, in MetaRocq.Template.Lib]
( _ ; _ ; _ ; _ ; _ ; _ ) [notation, in MetaRocq.Utils.MRPrelude]
( _ ; _ ; _ ; _ ; _ ) [notation, in MetaRocq.Utils.MRPrelude]
( _ ; _ ; _ ; _ ) [notation, in MetaRocq.Utils.MRPrelude]
( _ ; _ ; _ ) [notation, in MetaRocq.Utils.MRPrelude]
( _ ; _ ) [notation, in MetaRocq.Utils.MRPrelude]
() [notation, in MetaRocq.Template.Checker]
(=_cs) [notation, in MetaRocq.Common.Universes]
(=_cset) [notation, in MetaRocq.Common.Universes]
(=_lset) [notation, in MetaRocq.Common.Universes]
(=_g) [notation, in MetaRocq.Common.uGraph]
(=_gcs) [notation, in MetaRocq.Common.uGraph]
(==_cs) [notation, in MetaRocq.Common.Universes]
(==_cset) [notation, in MetaRocq.Common.Universes]
(==_lset) [notation, in MetaRocq.Common.Universes]
(⊂_cs) [notation, in MetaRocq.Common.Universes]
(⊂?_cs) [notation, in MetaRocq.Common.Universes]
<# _ #> [notation, in MetaRocq.Template.Loader]
<# _ #> [notation, in MetaRocq.TemplatePCUIC.Loader]
<%% _ %%> [notation, in MetaRocq.Erasure.Typed.Utils]
<% _ %> [notation, in MetaRocq.Template.Loader]
<% _ %> [notation, in MetaRocq.TemplatePCUIC.Loader]
`=1` [notation, in MetaRocq.Utils.MRPrelude]
`=2` [notation, in MetaRocq.Utils.MRPrelude]
`≡Γ` [notation, in MetaRocq.PCUIC.PCUICAlpha]
`≡α` [notation, in MetaRocq.PCUIC.PCUICAlpha]
¬ _ [notation, in MetaRocq.PCUIC.PCUICProgress]
⇑ _ [notation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
∥ _ ∥ [notation, in MetaRocq.Utils.MRSquash]
⊩ _ ~ _ [notation, in MetaRocq.Erasure.EWcbvEvalNamed]
⋆ [notation, in MetaRocq.PCUIC.PCUICInductiveInversion]
⎩ _ ⎭ [notation, in MetaRocq.Common.uGraph]
Σudecl [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
Σudecl_ref [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
Σ' [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Σ' [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Σ' [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
| 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) |