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 (lemma)
udecl_prop_in_var_poly [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]uip_bool [in MetaCoq.Template.utils.MCUtils]
uip_preservation [in MetaCoq.Translations.param_generous_packed]
unfold_length [in MetaCoq.Template.utils.MCList]
unfold_one_proj_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_proj_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_decompose [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zippx [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zipp [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_cofix_wf [in MetaCoq.Template.TypingWf]
unfold_fix_wf [in MetaCoq.Template.TypingWf]
unfold_cofix_type [in MetaCoq.Erasure.Prelim]
unique_sorting_equality_propositional [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_r [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_l [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_r [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_l [in MetaCoq.PCUIC.PCUICElimination]
UnivConstraint.compare_spec [in MetaCoq.Template.Universes]
UnivConstraint.eq_dec [in MetaCoq.Template.Universes]
UnivConstraint.lt_compat [in MetaCoq.Template.Universes]
UnivConstraint.lt_strorder [in MetaCoq.Template.Universes]
Universe.eqb_refl [in MetaCoq.Template.Universes]
Universe.make_inj [in MetaCoq.Template.Universes]
Universe.val_make [in MetaCoq.Template.Universes]
univ_is_prop_make [in MetaCoq.PCUIC.PCUICCumulProp]
univ_exprs_map_all [in MetaCoq.PCUIC.PCUICCumulProp]
univ_epxrs_elements_map [in MetaCoq.PCUIC.PCUICCumulProp]
univ_expr_set_in_elements [in MetaCoq.PCUIC.PCUICCumulProp]
untyped_substitution_red [in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_length [in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_nth_error [in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_projs [in MetaCoq.PCUIC.PCUICInductives]
untyped_subslet_inds [in MetaCoq.PCUIC.PCUICCumulProp]
untyped_subslet_inds [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_length [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_lift [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ass [in MetaCoq.PCUIC.PCUICConvCumInversion]
untyped_substitution_ws_cumul_pb_subst_conv' [in MetaCoq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb_subst_conv [in MetaCoq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
untyped_closed_red_subst [in MetaCoq.PCUIC.PCUICConversion]
untyped_subslet_def_tip [in MetaCoq.PCUIC.PCUICConversion]
untyped_subslet_extended_subst [in MetaCoq.PCUIC.PCUICContexts]
untyped_subslet_lift [in MetaCoq.PCUIC.PCUICContexts]
untyped_subslet_eq_subst [in MetaCoq.PCUIC.PCUICSpine]
untyped_subslet_skipn [in MetaCoq.PCUIC.PCUICSpine]
Upn_subst_consn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_ge [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_comp [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_S [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_1 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren_r [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren_l [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_proper [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_eq [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_1_Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_0 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
upn_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Upn_ctxmap [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
upto_names_impl_leq_term [in MetaCoq.PCUIC.PCUICEquality]
upto_names_impl_eq_term [in MetaCoq.PCUIC.PCUICEquality]
upto_names_impl [in MetaCoq.PCUIC.PCUICEquality]
upto_eq_impl [in MetaCoq.PCUIC.PCUICEquality]
upto_names_eq_term [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_leq_term [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_eq_term_upto_univ [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_eq_term_refl [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_conv_context [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_check_cofix [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_check_fix [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_destInd [in MetaCoq.PCUIC.PCUICAlpha]
Up_comp [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext_closed [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_up_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Up_Up_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext_cond [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
up_0 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Up_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Up_ctxmap [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
urename_is_open_term [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urename_on_free_vars_shift [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urenaming_strengthen [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
urenaming_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_ext [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vdef [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vass [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_impl [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
usubst_well_subst [in MetaCoq.PCUIC.PCUICSubstitution]
usubst_up_vdef [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_up_vass [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_app_up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_app [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_Up' [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_Up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_ext [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_on_free_vars_shift [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
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) |