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) |
U (definition)
UA [in MetaCoq.Translations.times_bool_fun]UA [in MetaCoq.Translations.times_bool_fun2]
UA_postcomposeequiv' [in MetaCoq.Translations.times_bool_fun2]
UA_postcomposeequiv [in MetaCoq.Translations.times_bool_fun2]
UContext.constraints [in MetaCoq.Template.Universes]
UContext.dest [in MetaCoq.Template.Universes]
UContext.empty [in MetaCoq.Template.Universes]
UContext.instance [in MetaCoq.Template.Universes]
UContext.make [in MetaCoq.Template.Universes]
UContext.make' [in MetaCoq.Template.Universes]
UContext.t [in MetaCoq.Template.Universes]
uctx_of_udecl [in MetaCoq.Template.common.uGraph]
uctx_invariants [in MetaCoq.Template.common.uGraph]
uint_wB [in MetaCoq.Template.BasicAst]
uint_size [in MetaCoq.Template.BasicAst]
uint63_model [in MetaCoq.Template.BasicAst]
uint63_to_model [in MetaCoq.PCUIC.TemplateToPCUIC]
uint63_from_model [in MetaCoq.PCUIC.PCUICToTemplate]
UIP [in MetaCoq.Translations.times_bool_fun]
UIP [in MetaCoq.Translations.param_generous_packed]
unfold [in MetaCoq.Template.utils.MCList]
unfold_cofix [in MetaCoq.Template.Typing]
unfold_fix [in MetaCoq.Template.Typing]
unfold_cofix [in MetaCoq.PCUIC.Syntax.PCUICCases]
unfold_fix [in MetaCoq.PCUIC.Syntax.PCUICCases]
unfold_one_proj [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_constants [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case [in MetaCoq.Template.Checker]
unfold_one_fix [in MetaCoq.Template.Checker]
unfold_cofix [in MetaCoq.Erasure.EGlobalEnv]
unfold_fix [in MetaCoq.Erasure.EGlobalEnv]
univ [in MetaCoq.Examples.typing_correctness]
univ [in MetaCoq.Examples.metacoq_tour_prelude]
UnivConstraint.compare [in MetaCoq.Template.Universes]
UnivConstraint.eq [in MetaCoq.Template.Universes]
UnivConstraint.eq_leibniz [in MetaCoq.Template.Universes]
UnivConstraint.eq_equiv [in MetaCoq.Template.Universes]
UnivConstraint.lt [in MetaCoq.Template.Universes]
UnivConstraint.make [in MetaCoq.Template.Universes]
UnivConstraint.t [in MetaCoq.Template.Universes]
universes_entry_of_decl [in MetaCoq.Template.Universes]
universes_graph [in MetaCoq.Template.common.uGraph]
Universe.add_list_to_exprs [in MetaCoq.Template.Universes]
Universe.add_to_exprs [in MetaCoq.Template.Universes]
Universe.eqb [in MetaCoq.Template.Universes]
Universe.from_kernel_repr [in MetaCoq.Template.Universes]
Universe.get_is_level [in MetaCoq.Template.Universes]
Universe.get_univ_exprs [in MetaCoq.Template.Universes]
Universe.is_type_sort [in MetaCoq.Template.Universes]
Universe.is_prop [in MetaCoq.Template.Universes]
Universe.is_sprop [in MetaCoq.Template.Universes]
Universe.is_level [in MetaCoq.Template.Universes]
Universe.is_levels [in MetaCoq.Template.Universes]
Universe.make [in MetaCoq.Template.Universes]
Universe.of_levels [in MetaCoq.Template.Universes]
Universe.of_expr [in MetaCoq.Template.Universes]
Universe.on_sort [in MetaCoq.Template.Universes]
Universe.sort_of_product [in MetaCoq.Template.Universes]
Universe.sup [in MetaCoq.Template.Universes]
Universe.super [in MetaCoq.Template.Universes]
Universe.t [in MetaCoq.Template.Universes]
Universe.to_cuniv [in MetaCoq.Template.Universes]
Universe.type0 [in MetaCoq.Template.Universes]
Universe.type1 [in MetaCoq.Template.Universes]
unlift [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
unlift_renaming [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
unlift_opt_pred [in MetaCoq.Template.Typing]
unlift_opt_pred [in MetaCoq.PCUIC.PCUICTyping]
Unnamed_thm0 [in MetaCoq.Examples.constructor_tac]
Unnamed_thm [in MetaCoq.Examples.constructor_tac]
Unnamed_thm [in MetaCoq.Translations.times_bool_fun2]
Unnamed_thm [in MetaCoq.Translations.param_generous_packed]
unpack_sigma [in MetaCoq.Translations.MiniHoTT]
unpack_sigma [in MetaCoq.Translations.MiniHoTT_paths]
up [in MetaCoq.Template.EtaExpand]
Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up [in MetaCoq.Erasure.ELiftSubst]
up [in MetaCoq.Template.LiftSubst]
Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
upto_names [in MetaCoq.PCUIC.PCUICEquality]
urenaming [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
usubst [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
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) |