| 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 (definition)
safe_nth [in MetaRocq.Utils.MRList]safe_hd [in MetaRocq.Erasure.EUnboxing]
safe_erasure_config [in MetaRocq.ErasurePlugin.Erasure]
same_typing_result [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_ind_comp [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_sort_comp [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_comp [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_typing_result_comp [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [in MetaRocq.Erasure.ErasureFunctionProperties]
same_cstr_info [in MetaRocq.Template.EtaExpand]
satisfies [in MetaRocq.Common.Universes]
satisfies0_sind [in MetaRocq.Common.Universes]
satisfies0_ind [in MetaRocq.Common.Universes]
sem [in MetaRocq.Examples.tauto]
semGen [in MetaRocq.Examples.tauto]
seq_size [in MetaRocq.Examples.tauto]
set_pparams_two [in MetaRocq.PCUIC.utils.PCUICOnOne]
set_pparams [in MetaRocq.PCUIC.utils.PCUICOnOne]
set_preturn_two [in MetaRocq.PCUIC.utils.PCUICOnOne]
set_preturn [in MetaRocq.PCUIC.utils.PCUICOnOne]
set_pcontext_two [in MetaRocq.PCUIC.utils.PCUICOnOne]
set_pcontext [in MetaRocq.PCUIC.utils.PCUICOnOne]
set_used [in MetaRocq.Erasure.Typed.Optimize]
set_preturn_two [in MetaRocq.PCUIC.PCUICConversion]
set_puinst [in MetaRocq.PCUIC.PCUICConversion]
set_array_value [in MetaRocq.PCUIC.PCUICReduction]
set_array_type [in MetaRocq.PCUIC.PCUICReduction]
set_array_default [in MetaRocq.PCUIC.PCUICReduction]
shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftf [in MetaRocq.PCUIC.PCUICAst]
shiftk [in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftnP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_predU [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
SingletonProp [in MetaRocq.PCUIC.PCUICElimination]
singleton_elim [in MetaRocq.Examples.metarocq_tour]
six [in MetaRocq.Examples.demo]
size [in MetaRocq.Examples.tauto]
size [in MetaRocq.PCUIC.utils.PCUICSize]
size [in MetaRocq.Utils.All_Forall]
size [in MetaRocq.Erasure.EInduction]
smash_telescope [in MetaRocq.SafeChecker.PCUICSafeChecker]
snd_eq [in MetaRocq.Utils.MRProd]
snoc [in MetaRocq.Common.BasicAst]
snoc [in MetaRocq.Erasure.EAst]
snoc_view_sind [in MetaRocq.Utils.MRList]
snoc_view_rec [in MetaRocq.Utils.MRList]
snoc_view_ind [in MetaRocq.Utils.MRList]
snoc_view_rect [in MetaRocq.Utils.MRList]
Sn_plus_one_transparent [in MetaRocq.Erasure.Typed.TypeAnnotations]
sort_of_type [in MetaRocq.SafeChecker.PCUICSafeRetyping]
sort_of_products [in MetaRocq.PCUIC.PCUICArities]
Sort.clt [in MetaRocq.Common.Universes]
Sort.csort_of_product [in MetaRocq.Common.Universes]
Sort.csup [in MetaRocq.Common.Universes]
Sort.csuper [in MetaRocq.Common.Universes]
Sort.eqb [in MetaRocq.Common.Universes]
Sort.family_sind [in MetaRocq.Common.Universes]
Sort.family_rec [in MetaRocq.Common.Universes]
Sort.family_ind [in MetaRocq.Common.Universes]
Sort.family_rect [in MetaRocq.Common.Universes]
Sort.get_is_level [in MetaRocq.Common.Universes]
Sort.is_type_sort [in MetaRocq.Common.Universes]
Sort.is_propositional [in MetaRocq.Common.Universes]
Sort.is_prop [in MetaRocq.Common.Universes]
Sort.is_sprop [in MetaRocq.Common.Universes]
Sort.is_level [in MetaRocq.Common.Universes]
Sort.is_levels [in MetaRocq.Common.Universes]
Sort.lt [in MetaRocq.Common.Universes]
Sort.lt__sind [in MetaRocq.Common.Universes]
Sort.lt__ind [in MetaRocq.Common.Universes]
Sort.map [in MetaRocq.Common.Universes]
Sort.of_levels [in MetaRocq.Common.Universes]
Sort.on_sort [in MetaRocq.Common.Universes]
Sort.OT.compare [in MetaRocq.Common.Universes]
Sort.OT.eq [in MetaRocq.Common.Universes]
Sort.OT.eq_dec [in MetaRocq.Common.Universes]
Sort.OT.eq_equiv [in MetaRocq.Common.Universes]
Sort.OT.lt [in MetaRocq.Common.Universes]
Sort.OT.lt_compat [in MetaRocq.Common.Universes]
Sort.OT.t [in MetaRocq.Common.Universes]
Sort.sort_of_product [in MetaRocq.Common.Universes]
Sort.sort_of_product_ [in MetaRocq.Common.Universes]
Sort.sup [in MetaRocq.Common.Universes]
Sort.super [in MetaRocq.Common.Universes]
Sort.super_ [in MetaRocq.Common.Universes]
Sort.sup_ [in MetaRocq.Common.Universes]
Sort.t [in MetaRocq.Common.Universes]
Sort.to_csort [in MetaRocq.Common.Universes]
Sort.to_family [in MetaRocq.Common.Universes]
Sort.type0 [in MetaRocq.Common.Universes]
Sort.type1 [in MetaRocq.Common.Universes]
Sort.t__sind [in MetaRocq.Common.Universes]
Sort.t__rec [in MetaRocq.Common.Universes]
Sort.t__ind [in MetaRocq.Common.Universes]
Sort.t__rect [in MetaRocq.Common.Universes]
spine [in MetaRocq.Erasure.EAstUtils]
split_suffix [in MetaRocq.Utils.MRList]
split_prefix [in MetaRocq.Utils.MRList]
split_at [in MetaRocq.Utils.MRList]
split_at_aux [in MetaRocq.Utils.MRList]
split_common_prefix [in MetaRocq.Quotation.CommonUtils]
split_modpath [in MetaRocq.Quotation.CommonUtils]
split_common_prefix_ls [in MetaRocq.Quotation.CommonUtils]
sq_ws_cumul_pb [in MetaRocq.PCUIC.PCUICConversion]
sr_stmt [in MetaRocq.PCUIC.PCUICSR]
SR_red1 [in MetaRocq.PCUIC.PCUICSR]
stack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_pos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position [in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_entry_choice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_context [in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_entry_context [in MetaRocq.PCUIC.Syntax.PCUICPosition]
stateR_sind [in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_ind [in MetaRocq.SafeChecker.PCUICSafeConversion]
state_sind [in MetaRocq.SafeChecker.PCUICSafeConversion]
state_rec [in MetaRocq.SafeChecker.PCUICSafeConversion]
state_ind [in MetaRocq.SafeChecker.PCUICSafeConversion]
state_rect [in MetaRocq.SafeChecker.PCUICSafeConversion]
strengthenP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
strictest_checker_flags [in MetaRocq.Common.config]
strictly_extends_decls_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
StringOT.compare [in MetaRocq.Utils.bytestring]
StringOT.eq [in MetaRocq.Utils.bytestring]
StringOT.eq_leibniz [in MetaRocq.Utils.bytestring]
StringOT.eq_dec [in MetaRocq.Utils.bytestring]
StringOT.eq_equiv [in MetaRocq.Utils.bytestring]
StringOT.lt [in MetaRocq.Utils.bytestring]
StringOT.lt_compat [in MetaRocq.Utils.bytestring]
StringOT.lt_irreflexive [in MetaRocq.Utils.bytestring]
StringOT.t [in MetaRocq.Utils.bytestring]
string_of_universe_instance [in MetaRocq.Common.Universes]
string_of_sort [in MetaRocq.Common.Universes]
string_of_level_expr [in MetaRocq.Common.Universes]
string_of_level [in MetaRocq.Common.Universes]
string_of_term [in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_term [in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_def [in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_branch [in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_predicate [in MetaRocq.Template.AstUtils]
string_of_pstring [in MetaRocq.Utils.Show]
string_of_float [in MetaRocq.Utils.Show]
string_of_prim_int [in MetaRocq.Utils.Show]
string_of_specfloat [in MetaRocq.Utils.Show]
string_of_option [in MetaRocq.Utils.Show]
string_of_bool [in MetaRocq.Utils.Show]
string_show [in MetaRocq.Utils.Show]
string_of_env_error [in MetaRocq.SafeChecker.PCUICErrors]
string_of_type_error [in MetaRocq.SafeChecker.PCUICErrors]
string_of_conv_error [in MetaRocq.SafeChecker.PCUICErrors]
string_of_conv_pb [in MetaRocq.SafeChecker.PCUICErrors]
string_of_Z [in MetaRocq.SafeChecker.PCUICErrors]
string_of_Z [in MetaRocq.Utils.MRString]
string_of_positive [in MetaRocq.Utils.MRString]
string_of_nat [in MetaRocq.Utils.MRString]
string_of_uint [in MetaRocq.Utils.MRString]
string_of_list [in MetaRocq.Utils.MRString]
string_of_list_aux [in MetaRocq.Utils.MRString]
string_of_term [in MetaRocq.PCUIC.utils.PCUICAstUtils]
string_of_aname [in MetaRocq.PCUIC.utils.PCUICAstUtils]
string_of_uint63_model [in MetaRocq.Common.BasicAst]
string_of_def [in MetaRocq.Common.BasicAst]
string_of_case_info [in MetaRocq.Common.BasicAst]
string_of_relevance [in MetaRocq.Common.BasicAst]
string_of_name [in MetaRocq.Common.BasicAst]
string_of_predicate [in MetaRocq.PCUIC.PCUICAst]
string_of_branch [in MetaRocq.PCUIC.PCUICAst]
string_of_type_error [in MetaRocq.Template.Checker]
string_of_gref [in MetaRocq.Common.Kernames]
string_of_inductive [in MetaRocq.Common.Kernames]
string_of_kername [in MetaRocq.Common.Kernames]
string_of_modpath [in MetaRocq.Common.Kernames]
string_of_dirpath [in MetaRocq.Common.Kernames]
string_of_branch [in MetaRocq.Template.Ast]
string_of_predicate [in MetaRocq.Template.Ast]
string_of_prim [in MetaRocq.Erasure.EPrimitive]
string_of_prim [in MetaRocq.PCUIC.utils.PCUICPrimitive]
string_of_term [in MetaRocq.Erasure.EAstUtils]
string_of_def [in MetaRocq.Erasure.EAstUtils]
String.append [in MetaRocq.Utils.bytestring]
String.compare [in MetaRocq.Utils.bytestring]
String.concat [in MetaRocq.Utils.bytestring]
String.contains [in MetaRocq.Utils.bytestring]
String.eqb [in MetaRocq.Utils.bytestring]
String.index [in MetaRocq.Utils.bytestring]
String.length [in MetaRocq.Utils.bytestring]
String.of_string [in MetaRocq.Utils.bytestring]
String.parse [in MetaRocq.Utils.bytestring]
String.prefix [in MetaRocq.Utils.bytestring]
String.print [in MetaRocq.Utils.bytestring]
String.rev [in MetaRocq.Utils.bytestring]
String.substring [in MetaRocq.Utils.bytestring]
String.to_string [in MetaRocq.Utils.bytestring]
String.t_sind [in MetaRocq.Utils.bytestring]
String.t_rec [in MetaRocq.Utils.bytestring]
String.t_ind [in MetaRocq.Utils.bytestring]
String.t_rect [in MetaRocq.Utils.bytestring]
strip [in MetaRocq.Erasure.ERemoveParams]
strip_outer_cast [in MetaRocq.Template.AstUtils]
strip_casts [in MetaRocq.Template.AstUtils]
strip_env' [in MetaRocq.Erasure.ERemoveParams]
strip_program [in MetaRocq.Erasure.ERemoveParams]
strip_env [in MetaRocq.Erasure.ERemoveParams]
strip_decl [in MetaRocq.Erasure.ERemoveParams]
strip_inductive_decl [in MetaRocq.Erasure.ERemoveParams]
strip_constant_decl [in MetaRocq.Erasure.ERemoveParams]
subgoal [in MetaRocq.Examples.tauto]
Subsingleton [in MetaRocq.PCUIC.PCUICElimination]
subslet_sind [in MetaRocq.PCUIC.PCUICSubstitution]
subslet_rec [in MetaRocq.PCUIC.PCUICSubstitution]
subslet_ind [in MetaRocq.PCUIC.PCUICSubstitution]
subslet_rect [in MetaRocq.PCUIC.PCUICSubstitution]
subst [in MetaRocq.PCUIC.PCUICAst]
subst [in MetaRocq.Template.Ast]
subst [in MetaRocq.Erasure.ELiftSubst]
substitutionT [in MetaRocq.PCUIC.PCUICSigmaCalculus]
substl [in MetaRocq.Erasure.ECSubst]
substl [in MetaRocq.Template.WcbvEval]
substl [in MetaRocq.PCUIC.PCUICWcbvEval]
substP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
subst_mutual_inductive_body [in MetaRocq.PCUIC.PCUICSubstitution]
subst_instance_mfix [in MetaRocq.PCUIC.PCUICGuardCondition]
subst_let_expand_tInd [in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_mkApps [in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_tProd [in MetaRocq.PCUIC.PCUICContexts]
subst_context_let_expand [in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand [in MetaRocq.PCUIC.PCUICContexts]
subst_app [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_gen [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_compose [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_fn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_let_expand_k [in MetaRocq.PCUIC.PCUICInductives]
subst_instance_valuation [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_context [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
subst1 [in MetaRocq.PCUIC.PCUICAst]
subst1 [in MetaRocq.Template.Ast]
subst1 [in MetaRocq.Erasure.ELiftSubst]
subs_sind [in MetaRocq.PCUIC.PCUICSubstitution]
subs_rec [in MetaRocq.PCUIC.PCUICSubstitution]
subs_ind [in MetaRocq.PCUIC.PCUICSubstitution]
subs_rect [in MetaRocq.PCUIC.PCUICSubstitution]
sub_context_set [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sum_deriv_lengths [in MetaRocq.Erasure.Typed.WcbvEvalAux]
sunny [in MetaRocq.Erasure.EWcbvEvalNamed]
swap [in MetaRocq.Utils.MRProd]
switch_off_box [in MetaRocq.Erasure.EImplementBox]
switch_cstr_as_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
switch_constructor_as_block [in MetaRocq.Erasure.EConstructorsAsBlocks]
switch_unguarded_fix [in MetaRocq.Erasure.EWcbvEval]
switch_env_flags_to_named [in MetaRocq.Erasure.EWcbvEvalNamed]
switch_term_flags_to_named [in MetaRocq.Erasure.EWcbvEvalNamed]
switch_no_params [in MetaRocq.Erasure.EInlineProjections]
switch_no_params [in MetaRocq.Erasure.ERemoveParams]
| 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) |