| 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) |
U
UContext [module, in MetaRocq.Common.Universes]UContext.constraints [definition, in MetaRocq.Common.Universes]
UContext.dest [definition, in MetaRocq.Common.Universes]
UContext.empty [definition, in MetaRocq.Common.Universes]
UContext.instance [definition, in MetaRocq.Common.Universes]
UContext.make [definition, in MetaRocq.Common.Universes]
UContext.make' [definition, in MetaRocq.Common.Universes]
UContext.t [definition, in MetaRocq.Common.Universes]
uctx_of_udecl [definition, in MetaRocq.Common.uGraph]
uctx_invariants [definition, in MetaRocq.Common.uGraph]
uctx' [definition, in MetaRocq.Common.uGraph]
uctx'_eq [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
udecl_prop_in_var_poly [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
uGraph [library]
uint_wB [definition, in MetaRocq.Common.BasicAst]
uint_size [definition, in MetaRocq.Common.BasicAst]
uint63_to_model [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
uint63_model [definition, in MetaRocq.Common.BasicAst]
uint63_from_model [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
uip_bool [lemma, in MetaRocq.Utils.MRUtils]
UnboundEvar [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UnboundEvar [constructor, in MetaRocq.Template.Checker]
UnboundMeta [constructor, in MetaRocq.Template.Checker]
UnboundRel [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UnboundRel [constructor, in MetaRocq.Template.Checker]
UnboundVar [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UnboundVar [constructor, in MetaRocq.Template.Checker]
unbox [definition, in MetaRocq.Erasure.EUnboxing]
unbox [section, in MetaRocq.Erasure.EUnboxing]
unboxable [definition, in MetaRocq.Erasure.EUnboxing]
unboxing [projection, in MetaRocq.ErasurePlugin.Erasure]
unbox_program [definition, in MetaRocq.Erasure.EUnboxing]
unbox_env [definition, in MetaRocq.Erasure.EUnboxing]
unbox_decl [definition, in MetaRocq.Erasure.EUnboxing]
unbox_inductive_decl [definition, in MetaRocq.Erasure.EUnboxing]
unbox_constant_decl [definition, in MetaRocq.Erasure.EUnboxing]
unbox_transformation [definition, in MetaRocq.ErasurePlugin.ETransform]
unbox.Def [section, in MetaRocq.Erasure.EUnboxing]
_ eqn: _ [notation, in MetaRocq.Erasure.EUnboxing]
unbox.Σ [variable, in MetaRocq.Erasure.EUnboxing]
UndeclaredConstant [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UndeclaredConstant [constructor, in MetaRocq.Template.Checker]
UndeclaredConstructor [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UndeclaredConstructor [constructor, in MetaRocq.Template.Checker]
UndeclaredInductive [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UndeclaredInductive [constructor, in MetaRocq.Template.Checker]
uneta_byte [definition, in MetaRocq.Utils.ByteCompareSpec]
unfold [definition, in MetaRocq.Utils.MRList]
unfold [constructor, in MetaRocq.Template.TemplateMonad.Common]
unfolds_bound [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
unfold_cofix_type [lemma, in MetaRocq.Erasure.Prelim]
unfold_length [lemma, in MetaRocq.Utils.MRList]
unfold_cofix [definition, in MetaRocq.Template.Typing]
unfold_fix [definition, in MetaRocq.Template.Typing]
unfold_one_case [definition, in MetaRocq.Template.Checker]
unfold_one_fix [definition, in MetaRocq.Template.Checker]
unfold_cofix_wf [lemma, in MetaRocq.Template.TypingWf]
unfold_fix_wf [lemma, in MetaRocq.Template.TypingWf]
unfold_cofix [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
unfold_fix [definition, in MetaRocq.PCUIC.Syntax.PCUICCases]
unfold_one_proj_None [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_proj_cored [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_proj [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_case_None [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_case_cored [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_case [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_constants [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_None [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_decompose [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_cored [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zippx [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zipp [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_one_fix [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
unfold_toplevel [definition, in MetaRocq.Template.Lib]
unfold_cofix [definition, in MetaRocq.Erasure.EGlobalEnv]
unfold_fix [definition, in MetaRocq.Erasure.EGlobalEnv]
union_checker_flags_spec [lemma, in MetaRocq.Common.config]
union_checker_flags [definition, in MetaRocq.Common.config]
UniquePose [library]
unique_sorting_equality_propositional [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_r [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_l [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_r [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_l [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_equality_prop [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_sorting_family [lemma, in MetaRocq.PCUIC.PCUICElimination]
unique_type [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
unique_decls [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
uniquify_valuation_for [definition, in MetaRocq.Common.UniversesDec]
uniquify_constraint_for [definition, in MetaRocq.Common.UniversesDec]
uniquify_level_for [definition, in MetaRocq.Common.UniversesDec]
uniquify_valuation [definition, in MetaRocq.Common.UniversesDec]
uniquify_constraint [definition, in MetaRocq.Common.UniversesDec]
uniquify_level [definition, in MetaRocq.Common.UniversesDec]
uniquify_level_var [definition, in MetaRocq.Common.UniversesDec]
uniquify_level_level [definition, in MetaRocq.Common.UniversesDec]
unit_FinitelyListablePackage [instance, in MetaRocq.Utils.MRListable]
Univ [section, in MetaRocq.Common.Universes]
univ [definition, in MetaRocq.Examples.typing_correctness]
univ [definition, in MetaRocq.Examples.metarocq_tour_prelude]
UnivCF2 [section, in MetaRocq.Common.Universes]
UnivCF2.cf1 [variable, in MetaRocq.Common.Universes]
UnivCF2.cf2 [variable, in MetaRocq.Common.Universes]
UnivConstraint [module, in MetaRocq.Common.Universes]
UnivConstraint.compare [definition, in MetaRocq.Common.Universes]
UnivConstraint.compare_spec [lemma, in MetaRocq.Common.Universes]
UnivConstraint.eq [definition, in MetaRocq.Common.Universes]
UnivConstraint.eq_leibniz [definition, in MetaRocq.Common.Universes]
UnivConstraint.eq_dec [lemma, in MetaRocq.Common.Universes]
UnivConstraint.eq_equiv [definition, in MetaRocq.Common.Universes]
UnivConstraint.lt [definition, in MetaRocq.Common.Universes]
UnivConstraint.lt_compat [lemma, in MetaRocq.Common.Universes]
UnivConstraint.lt_strorder [lemma, in MetaRocq.Common.Universes]
UnivConstraint.lt__sind [definition, in MetaRocq.Common.Universes]
UnivConstraint.lt__ind [definition, in MetaRocq.Common.Universes]
UnivConstraint.lt_Level1 [constructor, in MetaRocq.Common.Universes]
UnivConstraint.lt_Cstr [constructor, in MetaRocq.Common.Universes]
UnivConstraint.lt_Level2 [constructor, in MetaRocq.Common.Universes]
UnivConstraint.lt_ [inductive, in MetaRocq.Common.Universes]
UnivConstraint.make [definition, in MetaRocq.Common.Universes]
UnivConstraint.t [definition, in MetaRocq.Common.Universes]
Universe [module, in MetaRocq.Common.Universes]
UniverseClosedSubst [section, in MetaRocq.Common.Universes]
UniverseClosedSubst [section, in MetaRocq.PCUIC.PCUICInductiveInversion]
UniverseLemmas [section, in MetaRocq.Common.Universes]
UniverseLemmas.cf [variable, in MetaRocq.Common.Universes]
Universes [library]
UniversesDec [library]
universes_entry_of_decl [definition, in MetaRocq.Common.Universes]
universes_entry_sind [definition, in MetaRocq.Common.Universes]
universes_entry_rec [definition, in MetaRocq.Common.Universes]
universes_entry_ind [definition, in MetaRocq.Common.Universes]
universes_entry_rect [definition, in MetaRocq.Common.Universes]
universes_entry [inductive, in MetaRocq.Common.Universes]
universes_decl_sind [definition, in MetaRocq.Common.Universes]
universes_decl_rec [definition, in MetaRocq.Common.Universes]
universes_decl_ind [definition, in MetaRocq.Common.Universes]
universes_decl_rect [definition, in MetaRocq.Common.Universes]
universes_decl [inductive, in MetaRocq.Common.Universes]
universes_graph [definition, in MetaRocq.Common.uGraph]
universe_get_is_level_correct [lemma, in MetaRocq.Common.Universes]
Universe.eq_dec_univ0 [instance, in MetaRocq.Common.Universes]
Universe.Evaluable [instance, in MetaRocq.Common.Universes]
Universe.exprs [definition, in MetaRocq.Common.Universes]
Universe.from_kernel_repr [definition, in MetaRocq.Common.Universes]
Universe.get_is_level [definition, in MetaRocq.Common.Universes]
Universe.is_level [definition, in MetaRocq.Common.Universes]
Universe.is_levels [definition, in MetaRocq.Common.Universes]
Universe.levelexprset_reflect [instance, in MetaRocq.Common.Universes]
Universe.lt [definition, in MetaRocq.Common.Universes]
Universe.lt_strorder [instance, in MetaRocq.Common.Universes]
Universe.lt_compat [definition, in MetaRocq.Common.Universes]
Universe.make [definition, in MetaRocq.Common.Universes]
Universe.make' [definition, in MetaRocq.Common.Universes]
Universe.make'_inj [lemma, in MetaRocq.Common.Universes]
Universe.succ [definition, in MetaRocq.Common.Universes]
Universe.sup [definition, in MetaRocq.Common.Universes]
Universe.t [definition, in MetaRocq.Common.Universes]
Universe.val_make' [lemma, in MetaRocq.Common.Universes]
Universe.val_make [lemma, in MetaRocq.Common.Universes]
UnivSubst [record, in MetaRocq.Common.Universes]
UnivSubst [inductive, in MetaRocq.Common.Universes]
UnivSubst [library]
univ_sup_assoc [lemma, in MetaRocq.Common.Universes]
univ_sup_idem [lemma, in MetaRocq.Common.Universes]
univ_exprs_map_all [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
univ_epxrs_elements_map [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
univ_expr_set_in_elements [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
Univ.cf [variable, in MetaRocq.Common.Universes]
unlift [definition, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
unlift_renaming [definition, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
unlift_opt_pred [definition, in MetaRocq.PCUIC.PCUICTyping]
unlift_opt_pred [definition, in MetaRocq.Template.Typing]
Unnamed_thm0 [definition, in MetaRocq.Examples.constructor_tac]
Unnamed_thm [definition, in MetaRocq.Examples.constructor_tac]
unsafe_passes [record, in MetaRocq.ErasurePlugin.Erasure]
UnsatisfiableConstraints [constructor, in MetaRocq.Template.Checker]
UnsatisfiedConstraints [constructor, in MetaRocq.SafeChecker.PCUICErrors]
UnsatisfiedConstraints [constructor, in MetaRocq.Template.Checker]
untyped_substitution_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_length [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_nth_error [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_sind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_rec [definition, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_ind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_rect [definition, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_cons_let_def [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_cons_let_ass [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_emptyslet [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet [inductive, in MetaRocq.PCUIC.PCUICSubstitution]
untyped_subslet_eq_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
untyped_subslet_skipn [lemma, in MetaRocq.PCUIC.PCUICSpine]
untyped_subslet_inds [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_length [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_lift [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
untyped_substitution_ws_cumul_pb_subst_conv' [lemma, in MetaRocq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb_subst_conv [lemma, in MetaRocq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
untyped_closed_red_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
untyped_subslet_def_tip [lemma, in MetaRocq.PCUIC.PCUICConversion]
untyped_subslet_extended_subst [lemma, in MetaRocq.PCUIC.PCUICContexts]
untyped_subslet_lift [lemma, in MetaRocq.PCUIC.PCUICContexts]
untyped_subslet_projs [lemma, in MetaRocq.PCUIC.PCUICInductives]
untyped_subslet_inds [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
untyped_subslet_ass [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
ununiquify_level__uniquify_level [lemma, in MetaRocq.Common.UniversesDec]
ununiquify_level_level__uniquify_level_level [lemma, in MetaRocq.Common.UniversesDec]
ununiquify_level_var__uniquify_level_var [lemma, in MetaRocq.Common.UniversesDec]
ununiquify_valuation [definition, in MetaRocq.Common.UniversesDec]
ununiquify_constraint [definition, in MetaRocq.Common.UniversesDec]
ununiquify_level [definition, in MetaRocq.Common.UniversesDec]
ununiquify_level_var [definition, in MetaRocq.Common.UniversesDec]
ununiquify_level_level [definition, in MetaRocq.Common.UniversesDec]
up [definition, in MetaRocq.Template.EtaExpand]
up [definition, in MetaRocq.Template.LiftSubst]
Up [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up [definition, in MetaRocq.Erasure.ELiftSubst]
update_ind_ctor_mask [definition, in MetaRocq.Erasure.Typed.Optimize]
update_mib_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
Upn [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_ge [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_compose [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_Upn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_comp [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_S [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_1 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_Up [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ren_r [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ren_l [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ren [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_proper [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_eq [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_1_Up [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_0 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ext [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Upn_ctxmap [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
Upn_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
upn_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
upto_names_impl_leq_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
upto_names_impl_eq_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
upto_names_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
upto_names_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
upto_names_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
upto_names_ref [instance, in MetaRocq.PCUIC.PCUICEquality]
upto_names' [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
upto_names [definition, in MetaRocq.PCUIC.PCUICEquality]
upto_eq_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
upto_names_eq_term [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_leq_term [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_eq_term_upto_univ [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_conv_context [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_check_cofix [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_check_fix [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_destInd [lemma, in MetaRocq.PCUIC.PCUICAlpha]
upto_names_terms_refl [instance, in MetaRocq.PCUIC.PCUICAlpha]
Up_comp [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_ext_closed [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_up_assoc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Up_Up_assoc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_Upn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_Up [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Up_ext [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_proper' [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_ext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
up_up [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
Up_ctxmap [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
up_ext_cond [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
up_0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
Up_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
urename_is_open_term [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urename_on_free_vars_shift [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urenaming [definition, in MetaRocq.PCUIC.Syntax.PCUICRenameDef]
urenaming_strengthen [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
urenaming_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vdef [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vass [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
urenaming_impl [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
UsualIsLeibniz [module, in MetaRocq.Utils.MRMSets]
UsualIsLeibniz.eq_leibniz [lemma, in MetaRocq.Utils.MRMSets]
usubst [definition, in MetaRocq.PCUIC.Syntax.PCUICInstDef]
usubst_well_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
usubst_up_vdef [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_up_vass [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_app_up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_Up' [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_Up [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
usubst_on_free_vars_shift [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
utils [library]
Utils [library]
| 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) |