| 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 | (75519 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 | (245 entries) |
| Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
other (notation)
_ ++ _ (bs_scope) [in MetaCoq.Template.utils.bytestring]_ ^-1 (equiv_scope) [in MetaCoq.Translations.MiniHoTT]
_ oE _ (equiv_scope) [in MetaCoq.Translations.MiniHoTT]
1 (equiv_scope) [in MetaCoq.Translations.MiniHoTT]
_ ^-1 (equiv_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ oE _ (equiv_scope) [in MetaCoq.Translations.MiniHoTT_paths]
1 (equiv_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ ,, _ (erasure) [in MetaCoq.Erasure.EAst]
_ { _ := _ } (erasure) [in MetaCoq.Erasure.ELiftSubst]
_ ..2 (fibration_scope) [in MetaCoq.Translations.MiniHoTT]
_ ..1 (fibration_scope) [in MetaCoq.Translations.MiniHoTT]
_ .2 (fibration_scope) [in MetaCoq.Translations.MiniHoTT]
_ .1 (fibration_scope) [in MetaCoq.Translations.MiniHoTT]
( _ ; _ ) (fibration_scope) [in MetaCoq.Translations.MiniHoTT]
_ ..2 (fibration_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ ..1 (fibration_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ .2 (fibration_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ .1 (fibration_scope) [in MetaCoq.Translations.MiniHoTT_paths]
( _ ; _ ) (fibration_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ ^-1 (function_scope) [in MetaCoq.Translations.MiniHoTT]
_ oD _ (function_scope) [in MetaCoq.Translations.MiniHoTT]
_ o _ (function_scope) [in MetaCoq.Translations.MiniHoTT]
_ ^-1 (function_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ oD _ (function_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ o _ (function_scope) [in MetaCoq.Translations.MiniHoTT_paths]
` _ (metacoq_scope) [in MetaCoq.SafeChecker.PCUICSafeReduce]
! (metacoq_scope) [in MetaCoq.Template.utils.MCPrelude]
_ .2 (pair_scope) [in MetaCoq.Template.utils.MCProd]
_ .1 (pair_scope) [in MetaCoq.Template.utils.MCProd]
_ @@ _ (path_scope) [in MetaCoq.Translations.MiniHoTT]
_ ^ (path_scope) [in MetaCoq.Translations.MiniHoTT]
_ @ _ (path_scope) [in MetaCoq.Translations.MiniHoTT]
_ # _ (path_scope) [in MetaCoq.Translations.MiniHoTT]
1 (path_scope) [in MetaCoq.Translations.MiniHoTT]
_ @@ _ (path_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ ^ (path_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ @ _ (path_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ # _ (path_scope) [in MetaCoq.Translations.MiniHoTT_paths]
1 (path_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ ⊢ _ ≤[ _ ] _ ✓ (pcuic) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ ≤ _ (pcuic) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ = _ (pcuic) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ ≤[ _ ] _ (pcuic) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ⊢ _ ⇝ _ (pcuic) [in MetaCoq.PCUIC.PCUICContextConversion]
( _ ; _ ) (prod_scope) [in MetaCoq.Translations.times_bool_fun]
_ .2 (sigma_scope) [in MetaCoq.Translations.sigma]
_ .1 (sigma_scope) [in MetaCoq.Translations.sigma]
( _ ; _ ) (sigma_scope) [in MetaCoq.Translations.sigma]
⇑^ _ _ (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ ⋅n _ (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
↑^ _ (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ ∘s _ (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
↑ (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ ⋅ _ (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ .[ _ ] (sigma_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ =2 _ (signature_scope) [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ ^ _ (string_scope2) [in MetaCoq.Template.utils]
_ ;;; _ |- _ ◃ _ (type_scope) [in MetaCoq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹{ _ } ( _ , _ ) (type_scope) [in MetaCoq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹Π ( _ , _ , _ ) (type_scope) [in MetaCoq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹□ _ (type_scope) [in MetaCoq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ ▹ _ (type_scope) [in MetaCoq.PCUIC.Bidirectional.BDTyping]
_ ;;; _ |- _ <= _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativity]
_ ;;; _ |- _ = _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativity]
_ ;;; _ |- _ <=[ _ ] _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativity]
_ × _ (type_scope) [in MetaCoq.Translations.times_bool_fun]
_ ;;; _ |- _ ~~ _ (type_scope) [in MetaCoq.Erasure.EArities]
_ ⊢p _ ▷ _ (type_scope) [in MetaCoq.Erasure.EArities]
wf_local _ _ (type_scope) [in MetaCoq.Template.Typing]
_ ;;; _ |- _ : _ (type_scope) [in MetaCoq.Template.Typing]
_ ;;; _ |- _ <= _ (type_scope) [in MetaCoq.Template.Typing]
_ ;;; _ |- _ = _ (type_scope) [in MetaCoq.Template.Typing]
_ ⊢ _ ▷ _ (type_scope) [in MetaCoq.Erasure.ErasureCorrectness]
_ |-p _ ▷ _ (type_scope) [in MetaCoq.Erasure.ErasureCorrectness]
_ ⊢ _ ▷ _ (type_scope) [in MetaCoq.Erasure.EDeps]
_ ;;; _ |-[ _ ] _ = _ (type_scope) [in MetaCoq.PCUIC.PCUICSubstitution]
_ ;;; _ |-[ _ ] _ <= _ (type_scope) [in MetaCoq.PCUIC.PCUICSubstitution]
_ ;;; _ |-[ _ ] _ <=[ _ ] _ (type_scope) [in MetaCoq.PCUIC.PCUICSubstitution]
_ * _ (type_scope2) [in MetaCoq.Template.utils]
_ ⊢ _ <==[ _ , _ ] _ (type_scope) [in MetaCoq.PCUIC.PCUICEquality]
_ × _ (type_scope) [in MetaCoq.Translations.sigma]
∃ _ .. _ , _ (type_scope) [in MetaCoq.Translations.sigma]
{ _ : _ && _ } (type_scope) [in MetaCoq.Translations.sigma]
{ _ && _ } (type_scope) [in MetaCoq.Translations.sigma]
_ ;;; _ ⊢ _ = _ (type_scope) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ;;; _ ⊢ _ ≤ _ (type_scope) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ;;; _ ⊢ _ ≤[ _ ] _ (type_scope) [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
() (type_scope) [in MetaCoq.Template.Checker]
_ <~> _ (type_scope) [in MetaCoq.Translations.MiniHoTT]
_ == _ (type_scope) [in MetaCoq.Translations.MiniHoTT]
_ = _ (type_scope) [in MetaCoq.Translations.MiniHoTT]
_ = _ :> _ (type_scope) [in MetaCoq.Translations.MiniHoTT]
{ _ : _ & _ } (type_scope) [in MetaCoq.Translations.MiniHoTT]
exists _ .. _ , _ (type_scope) [in MetaCoq.Translations.MiniHoTT]
_ ⊢ _ =s _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativitySpec]
_ ⊢ _ ≤s _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativitySpec]
_ ⊢ _ ≤s[ _ ] _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativitySpec]
_ ;;; _ ⊢ _ ≤s[ _ ] _ (type_scope) [in MetaCoq.PCUIC.PCUICCumulativitySpec]
[ × _ , _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ , _ , _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ , _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ , _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
[ × _ & _ ] (type_scope) [in MetaCoq.Template.utils.MCProd]
_ <~> _ (type_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ == _ (type_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ = _ (type_scope) [in MetaCoq.Translations.MiniHoTT_paths]
_ = _ :> _ (type_scope) [in MetaCoq.Translations.MiniHoTT_paths]
{ _ : _ & _ } (type_scope) [in MetaCoq.Translations.MiniHoTT_paths]
exists _ .. _ , _ (type_scope) [in MetaCoq.Translations.MiniHoTT_paths]
∑ _ .. _ , _ (type_scope) [in MetaCoq.Template.utils.MCPrelude]
_ × _ (type_scope) [in MetaCoq.Translations.param_generous_packed]
⟦ _ ⟧_ _ (univ_scope) [in MetaCoq.Template.Universes]
_ ?? _ [in MetaCoq.Template.utils.MCCompare]
_ @[ _ ] [in MetaCoq.Template.Universes]
_ ⊂_cs _ [in MetaCoq.Template.Universes]
_ =_cs _ [in MetaCoq.Template.Universes]
_ =_cset _ [in MetaCoq.Template.Universes]
_ =_lset _ [in MetaCoq.Template.Universes]
_ ,, _ [in MetaCoq.Template.BasicAst]
_ ⊢ _ <===[ _ ] _ [in MetaCoq.PCUIC.PCUICCumulativity]
_ <= _ [in MetaCoq.Translations.param_binary]
_ <~> _ [in MetaCoq.Template.utils.MCRelations]
_ ;;; _ |- _ <=[ _ ] _ [in MetaCoq.Template.Typing]
_ ⊨ _ \ _ by _ ⨷ _ [in MetaCoq.PCUIC.utils.PCUICUtils]
_ ⊗ _ [in MetaCoq.PCUIC.utils.PCUICUtils]
_ ⊩ _ ⨶ _ [in MetaCoq.PCUIC.utils.PCUICUtils]
_ ;;; _ |- _ = _ ✓ [in MetaCoq.PCUIC.PCUICSubstitution]
_ ;;; _ |- _ <= _ ✓ [in MetaCoq.PCUIC.PCUICSubstitution]
_ ;;; _ |- _ ⇝ℇ _ [in MetaCoq.Erasure.Extract]
_ { _ := _ } [in MetaCoq.Template.Ast]
_ =_g _ [in MetaCoq.Template.common.uGraph]
_ =_gcs _ [in MetaCoq.Template.common.uGraph]
_ # _ [in MetaCoq.Template.utils.MCEquality]
_ ≡' _ [in MetaCoq.PCUIC.PCUICEquality]
_ ≡ _ [in MetaCoq.PCUIC.PCUICEquality]
_ ∘i _ [in MetaCoq.PCUIC.PCUICSigmaCalculus]
_ ≡Γ _ [in MetaCoq.PCUIC.PCUICAlpha]
_ ≡α _ [in MetaCoq.PCUIC.PCUICAlpha]
_ == _ [in MetaCoq.Template.utils.ReflectEq]
_ ∼_ext _ [in MetaCoq.SafeChecker.PCUICWfEnv]
_ ∼ _ [in MetaCoq.SafeChecker.PCUICWfEnv]
_ { _ := _ } [in MetaCoq.PCUIC.PCUICAst]
_ ;;; _ ⊢ _ ⇝ _ [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
_ ==? _ [in MetaCoq.Template.Reflect]
_ ==? _ [in MetaCoq.Template.ReflectAst]
_ <= _ [in MetaCoq.Translations.standard_model]
_ ==? _ [in MetaCoq.PCUIC.Syntax.PCUICReflect]
_ ;;; _ |- _ : _ [in MetaCoq.PCUIC.PCUICTyping]
_ ;;; _ |- _ =s _ [in MetaCoq.PCUIC.PCUICCumulativitySpec]
_ ;;; _ |- _ <=s _ [in MetaCoq.PCUIC.PCUICCumulativitySpec]
_ .p2 [in MetaCoq.Template.utils.MCProd]
_ .p1 [in MetaCoq.Template.utils.MCProd]
_ × _ [in MetaCoq.Template.utils.MCProd]
_ ;;; _ ⊢ _ : _ [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
_ ;;; _ ⊢ _ ⇝1 _ [in MetaCoq.PCUIC.PCUICSR]
_ =2 _ [in MetaCoq.Template.utils.MCPrelude]
_ =1 _ [in MetaCoq.Template.utils.MCPrelude]
_ .π2 [in MetaCoq.Template.utils.MCPrelude]
_ .π1 [in MetaCoq.Template.utils.MCPrelude]
_ ∘ _ [in MetaCoq.Template.utils.MCPrelude]
_ <= _ [in MetaCoq.Translations.param_original]
_ ;;; _ |- _ ⇝* _ [in MetaCoq.PCUIC.PCUICReduction]
_ ;;; _ |- _ ⇝ _ [in MetaCoq.PCUIC.PCUICReduction]
El _ [in MetaCoq.Translations.param_cheap_packed]
El _ [in MetaCoq.Translations.param_generous_packed]
eta_compose [in MetaCoq.Template.utils.MCPrelude]
lens [in MetaCoq.PCUIC.Syntax.PCUICTactics]
precompose [in MetaCoq.Template.utils.MCRelations]
tsl_ty_param [in MetaCoq.Translations.param_cheap_packed]
tsl_ty_param [in MetaCoq.Translations.param_generous_packed]
TYPE [in MetaCoq.Translations.param_cheap_packed]
TYPE [in MetaCoq.Translations.param_generous_packed]
wf_local_bd_rel _ _ _ [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wf_local_bd _ _ [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wf_local _ _ [in MetaCoq.PCUIC.PCUICTyping]
!! _ [in MetaCoq.PCUIC.PCUICInductiveInversion]
#| _ | [in MetaCoq.Template.utils.MCList]
( _ ; _ ; _ ; _ ; _ ; _ ) [in MetaCoq.Template.utils.MCPrelude]
( _ ; _ ; _ ; _ ; _ ) [in MetaCoq.Template.utils.MCPrelude]
( _ ; _ ; _ ; _ ) [in MetaCoq.Template.utils.MCPrelude]
( _ ; _ ; _ ) [in MetaCoq.Template.utils.MCPrelude]
( _ ; _ ) [in MetaCoq.Template.utils.MCPrelude]
() [in MetaCoq.Template.Checker]
(=_cs) [in MetaCoq.Template.Universes]
(=_cset) [in MetaCoq.Template.Universes]
(=_lset) [in MetaCoq.Template.Universes]
(=_g) [in MetaCoq.Template.common.uGraph]
(=_gcs) [in MetaCoq.Template.common.uGraph]
(⊂_cs) [in MetaCoq.Template.Universes]
<% _ %> [in MetaCoq.Template.Loader]
`=1` [in MetaCoq.Template.utils.MCPrelude]
`=2` [in MetaCoq.Template.utils.MCPrelude]
`≡Γ` [in MetaCoq.PCUIC.PCUICAlpha]
`≡α` [in MetaCoq.PCUIC.PCUICAlpha]
⇑ _ [in MetaCoq.PCUIC.PCUICSigmaCalculus]
∥ _ ∥ [in MetaCoq.Template.utils.MCSquash]
⋆ [in MetaCoq.PCUIC.PCUICInductiveInversion]
⎩ _ ⎭ [in MetaCoq.Template.common.uGraph]
| 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 | (75519 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 | (245 entries) |
| Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |