| 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) |
S (instance)
satisfies_subsets [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]satisfies_equal_sets [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
shiftnP_ext [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftn_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
show_pstring [in MetaRocq.Utils.Show]
show_Z [in MetaRocq.Utils.Show]
show_positive [in MetaRocq.Utils.Show]
show_float [in MetaRocq.Utils.Show]
show_specfloat [in MetaRocq.Utils.Show]
show_sint [in MetaRocq.Utils.Show]
show_uint [in MetaRocq.Utils.Show]
show_list [in MetaRocq.Utils.Show]
show_option [in MetaRocq.Utils.Show]
show_sum [in MetaRocq.Utils.Show]
show_pair [in MetaRocq.Utils.Show]
show_bool [in MetaRocq.Utils.Show]
show_string [in MetaRocq.Utils.Show]
show_bytestring [in MetaRocq.Utils.Show]
show_program [in MetaRocq.PCUIC.utils.PCUICPretty]
show_env [in MetaRocq.PCUIC.utils.PCUICPretty]
Sort.eq_dec_sort [in MetaRocq.Common.Universes]
Sort.OT.lt_strorder [in MetaRocq.Common.Universes]
Sort.reflect_eq_sort [in MetaRocq.Common.Universes]
strengthenP_proper [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
StringOT.lt_strorder [in MetaRocq.Utils.bytestring]
StringOT.lt_transitive [in MetaRocq.Utils.bytestring]
StringOT.reflect_eq_string [in MetaRocq.Utils.bytestring]
string_eqdec [in MetaRocq.Utils.MRPrelude]
subgraph_proper [in MetaRocq.Common.uGraph]
subrelation_compare_sort_eq_prop [in MetaRocq.PCUIC.PCUICCumulProp]
subrel_extends_eq_le [in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_le [in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_eq [in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_eq_pb [in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_cmp [in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_cmp_universe [in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_config_impl_eq_le [in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_le [in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_eq [in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_eq_pb [in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_cmp [in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_lt_le [in MetaRocq.Utils.MRArith]
subrel_eq_le [in MetaRocq.Utils.MRArith]
subrel_R_True [in MetaRocq.PCUIC.PCUICCumulProp]
substu_pres_eq [in MetaRocq.PCUIC.PCUICSN]
substu_True_eq_univ_prop [in MetaRocq.PCUIC.PCUICCumulProp]
substu_f_True [in MetaRocq.PCUIC.PCUICCumulProp]
subst_instance_instance [in MetaRocq.Common.Universes]
subst_instance_sort [in MetaRocq.Common.Universes]
subst_instance_universe [in MetaRocq.Common.Universes]
subst_instance_level_expr [in MetaRocq.Common.Universes]
subst_instance_cstrs [in MetaRocq.Common.Universes]
subst_instance_cstr [in MetaRocq.Common.Universes]
subst_instance_level [in MetaRocq.Common.Universes]
subst_instance_list [in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_cons_gen_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_proper_ext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_compose_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_proper [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_instance_constr [in MetaRocq.PCUIC.PCUICAst]
subst_instance_mutual_inductive_body [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_inductive_body [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_constructor_body [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_nat [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_prod [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_def [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_constr [in MetaRocq.Template.Ast]
sub_context_set_trans [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sym_eq_univ_prop [in MetaRocq.PCUIC.PCUICCumulProp]
| 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) |