| 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) |
S (definition)
safe_nth [in MetaCoq.Template.utils.MCList]same_typing_result [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_ind_comp [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_sort_comp [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_comp [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_typing_result_comp [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [in MetaCoq.Erasure.ErasureFunction]
satisfies [in MetaCoq.Template.Universes]
Sect [in MetaCoq.Translations.MiniHoTT]
Sect [in MetaCoq.Translations.MiniHoTT_paths]
sem [in MetaCoq.Examples.tauto]
semGen [in MetaCoq.Examples.tauto]
seq_size [in MetaCoq.Examples.tauto]
set_pparams_two [in MetaCoq.PCUIC.utils.PCUICOnOne]
set_pparams [in MetaCoq.PCUIC.utils.PCUICOnOne]
set_preturn_two [in MetaCoq.PCUIC.utils.PCUICOnOne]
set_preturn [in MetaCoq.PCUIC.utils.PCUICOnOne]
set_pcontext_two [in MetaCoq.PCUIC.utils.PCUICOnOne]
set_pcontext [in MetaCoq.PCUIC.utils.PCUICOnOne]
set_preturn_two [in MetaCoq.PCUIC.PCUICConversion]
set_puinst [in MetaCoq.PCUIC.PCUICConversion]
shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftf [in MetaCoq.PCUIC.PCUICAst]
shiftk [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftnP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_predU [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
sigT_ind [in MetaCoq.Translations.MiniHoTT_paths]
SingletonProp [in MetaCoq.PCUIC.PCUICElimination]
singleton_elim [in MetaCoq.Examples.metacoq_tour]
six [in MetaCoq.Examples.demo]
size [in MetaCoq.Erasure.EInduction]
size [in MetaCoq.Template.utils.All_Forall]
size [in MetaCoq.Examples.tauto]
size [in MetaCoq.PCUIC.utils.PCUICSize]
smash_telescope [in MetaCoq.SafeChecker.PCUICSafeChecker]
snd_eq [in MetaCoq.Template.utils.MCProd]
snoc [in MetaCoq.Template.BasicAst]
snoc [in MetaCoq.Erasure.EAst]
sort_of_products [in MetaCoq.PCUIC.PCUICArities]
sort_of_type [in MetaCoq.SafeChecker.PCUICSafeRetyping]
spine [in MetaCoq.Erasure.EAstUtils]
split_suffix [in MetaCoq.Template.utils.MCList]
split_prefix [in MetaCoq.Template.utils.MCList]
split_at [in MetaCoq.Template.utils.MCList]
split_at_aux [in MetaCoq.Template.utils.MCList]
sq_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
sr_stmt [in MetaCoq.PCUIC.PCUICSR]
SR_red1 [in MetaCoq.PCUIC.PCUICSR]
stack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_pos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry_choice [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_context [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry_context [in MetaCoq.PCUIC.Syntax.PCUICPosition]
strengthenP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
StringOT.compare [in MetaCoq.Template.utils.bytestring]
StringOT.eq [in MetaCoq.Template.utils.bytestring]
StringOT.eq_leibniz [in MetaCoq.Template.utils.bytestring]
StringOT.eq_dec [in MetaCoq.Template.utils.bytestring]
StringOT.eq_equiv [in MetaCoq.Template.utils.bytestring]
StringOT.lt [in MetaCoq.Template.utils.bytestring]
StringOT.lt_compat [in MetaCoq.Template.utils.bytestring]
StringOT.lt_irreflexive [in MetaCoq.Template.utils.bytestring]
StringOT.t [in MetaCoq.Template.utils.bytestring]
string_of_universe_instance [in MetaCoq.Template.Universes]
string_of_sort [in MetaCoq.Template.Universes]
string_of_level_expr [in MetaCoq.Template.Universes]
string_of_level [in MetaCoq.Template.Universes]
string_of_float64_model [in MetaCoq.Template.BasicAst]
string_of_uint63_model [in MetaCoq.Template.BasicAst]
string_of_def [in MetaCoq.Template.BasicAst]
string_of_case_info [in MetaCoq.Template.BasicAst]
string_of_relevance [in MetaCoq.Template.BasicAst]
string_of_name [in MetaCoq.Template.BasicAst]
string_of_term [in MetaCoq.PCUIC.utils.PCUICAstUtils]
string_of_aname [in MetaCoq.PCUIC.utils.PCUICAstUtils]
string_of_branch [in MetaCoq.Template.Ast]
string_of_predicate [in MetaCoq.Template.Ast]
string_of_Z [in MetaCoq.Template.utils.MCString]
string_of_positive [in MetaCoq.Template.utils.MCString]
string_of_nat [in MetaCoq.Template.utils.MCString]
string_of_uint [in MetaCoq.Template.utils.MCString]
string_of_list [in MetaCoq.Template.utils.MCString]
string_of_list_aux [in MetaCoq.Template.utils.MCString]
string_of_gref [in MetaCoq.Template.Kernames]
string_of_inductive [in MetaCoq.Template.Kernames]
string_of_kername [in MetaCoq.Template.Kernames]
string_of_modpath [in MetaCoq.Template.Kernames]
string_of_dirpath [in MetaCoq.Template.Kernames]
string_repeat [in MetaCoq.SafeChecker.PCUICConsistency]
string_of_type_error [in MetaCoq.SafeChecker.PCUICErrors]
string_of_conv_error [in MetaCoq.SafeChecker.PCUICErrors]
string_of_conv_pb [in MetaCoq.SafeChecker.PCUICErrors]
string_of_Z [in MetaCoq.SafeChecker.PCUICErrors]
string_of_predicate [in MetaCoq.PCUIC.PCUICAst]
string_of_branch [in MetaCoq.PCUIC.PCUICAst]
string_of_type_error [in MetaCoq.Template.Checker]
string_of_term [in MetaCoq.Erasure.EAstUtils]
string_of_def [in MetaCoq.Erasure.EAstUtils]
string_of_prim [in MetaCoq.PCUIC.utils.PCUICPrimitive]
string_of_float64_model [in MetaCoq.PCUIC.utils.PCUICPrimitive]
string_of_term [in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_term [in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_def [in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_branch [in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_predicate [in MetaCoq.Template.AstUtils]
string_of_float [in MetaCoq.Template.AstUtils]
string_of_prim_int [in MetaCoq.Template.AstUtils]
String.append [in MetaCoq.Template.utils.bytestring]
String.compare [in MetaCoq.Template.utils.bytestring]
String.concat [in MetaCoq.Template.utils.bytestring]
String.contains [in MetaCoq.Template.utils.bytestring]
String.eqb [in MetaCoq.Template.utils.bytestring]
String.index [in MetaCoq.Template.utils.bytestring]
String.length [in MetaCoq.Template.utils.bytestring]
String.of_string [in MetaCoq.Template.utils.bytestring]
String.parse [in MetaCoq.Template.utils.bytestring]
String.prefix [in MetaCoq.Template.utils.bytestring]
String.print [in MetaCoq.Template.utils.bytestring]
String.rev [in MetaCoq.Template.utils.bytestring]
String.substring [in MetaCoq.Template.utils.bytestring]
String.to_string [in MetaCoq.Template.utils.bytestring]
strip [in MetaCoq.Erasure.ERemoveParams]
strip_env' [in MetaCoq.Erasure.ERemoveParams]
strip_program [in MetaCoq.Erasure.ERemoveParams]
strip_env [in MetaCoq.Erasure.ERemoveParams]
strip_decl [in MetaCoq.Erasure.ERemoveParams]
strip_inductive_decl [in MetaCoq.Erasure.ERemoveParams]
strip_constant_decl [in MetaCoq.Erasure.ERemoveParams]
strip_outer_cast [in MetaCoq.Template.AstUtils]
strip_casts [in MetaCoq.Template.AstUtils]
subgoal [in MetaCoq.Examples.tauto]
subst [in MetaCoq.Template.Ast]
subst [in MetaCoq.PCUIC.PCUICAst]
subst [in MetaCoq.Erasure.ELiftSubst]
substitution [in MetaCoq.PCUIC.PCUICSigmaCalculus]
substl [in MetaCoq.PCUIC.PCUICWcbvEval]
substl [in MetaCoq.Template.WcbvEval]
substl [in MetaCoq.Erasure.ECSubst]
substP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
subst_app [in MetaCoq.Translations.translation_utils]
subst_app [in MetaCoq.Translations.times_bool_fun]
subst_mutual_inductive_body [in MetaCoq.PCUIC.PCUICSubstitution]
subst_let_expand_k [in MetaCoq.PCUIC.PCUICInductives]
subst_app [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_gen [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_fn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_instance_valuation [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_let_expand_tInd [in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_mkApps [in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_tProd [in MetaCoq.PCUIC.PCUICContexts]
subst_context_let_expand [in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand [in MetaCoq.PCUIC.PCUICContexts]
subst1 [in MetaCoq.Template.Ast]
subst1 [in MetaCoq.PCUIC.PCUICAst]
subst1 [in MetaCoq.Erasure.ELiftSubst]
sub_context_set [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
suffix [in MetaCoq.Translations.param_binary]
suffix0 [in MetaCoq.Translations.param_binary]
swap [in MetaCoq.Template.utils.MCProd]
switch_no_params [in MetaCoq.Erasure.EInlineProjections]
switch_constructor_as_block [in MetaCoq.Erasure.EConstructorsAsBlocks]
switch_no_params [in MetaCoq.Erasure.ERemoveParams]
switch_unguarded_fix [in MetaCoq.Erasure.EWcbvEval]
| 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) |