Contents:
| 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 | (225 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 | (4 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 | (16 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 | (15 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 | (16 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 | (4 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 | (2 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 | (4 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 | (159 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 | (5 entries) |
Global Index
A
ack [definition, in RustExtraction.Test.InternalFix]any_type_symbol [projection, in RustExtraction.RustExtract]
append [definition, in RustExtraction.PrettyPrinterMonad]
append_concat [definition, in RustExtraction.PrettyPrinterMonad]
append_join [definition, in RustExtraction.PrettyPrinterMonad]
append_nl [definition, in RustExtraction.PrettyPrinterMonad]
B
BernsteinYangTermination [library]bs_to_s [abbreviation, in RustExtraction.PrettyPrinterMonad]
bs_to_s [abbreviation, in RustExtraction.RustExtract]
C
capitalize [definition, in RustExtraction.StringExtra]char_to_lower [definition, in RustExtraction.StringExtra]
char_to_upper [definition, in RustExtraction.StringExtra]
clean_local_ident [definition, in RustExtraction.RustExtract]
clean_global_ident [definition, in RustExtraction.RustExtract]
collect_output [definition, in RustExtraction.PrettyPrinterMonad]
collect_output_lines [definition, in RustExtraction.PrettyPrinterMonad]
Common [library]
const_global_ident_of_kername [definition, in RustExtraction.RustExtract]
cur_output_line [projection, in RustExtraction.PrettyPrinterMonad]
D
default_attrs [definition, in RustExtraction.Test.RustExtractTests]default_attrs [definition, in RustExtraction.PluginExtract]
divstep [definition, in RustExtraction.Test.BernsteinYangTermination]
E
E [module, in RustExtraction.RustExtract]EF [module, in RustExtraction.RustExtract]
even [definition, in RustExtraction.Test.InternalFix]
even_odd [definition, in RustExtraction.Test.InternalFix]
Ex [module, in RustExtraction.RustExtract]
extract [definition, in RustExtraction.Test.RustExtractTests]
extract [definition, in RustExtraction.PluginExtract]
ExtractExtraction [library]
extract_def_name_exists [definition, in RustExtraction.Common]
extract_rust_within_coq [definition, in RustExtraction.RustExtract]
extract_lines [definition, in RustExtraction.PluginExtract]
ExtrRustBasic [library]
ExtrRustCheckedArith [library]
ExtrRustUncheckedArith [library]
ex1 [module, in RustExtraction.Test.RustExtractTests]
ex1.bar [definition, in RustExtraction.Test.RustExtractTests]
ex1.ex1_test [definition, in RustExtraction.Test.RustExtractTests]
ex1.foo [definition, in RustExtraction.Test.RustExtractTests]
ex2 [module, in RustExtraction.Test.RustExtractTests]
ex2.bar [definition, in RustExtraction.Test.RustExtractTests]
ex2.ex2_test [definition, in RustExtraction.Test.RustExtractTests]
ex2.foo [definition, in RustExtraction.Test.RustExtractTests]
ex2.only_in_type [definition, in RustExtraction.Test.RustExtractTests]
ex3 [module, in RustExtraction.Test.RustExtractTests]
ex3.test [definition, in RustExtraction.Test.RustExtractTests]
ex4 [module, in RustExtraction.Test.RustExtractTests]
ex4.ack [definition, in RustExtraction.Test.RustExtractTests]
ex4.test [definition, in RustExtraction.Test.RustExtractTests]
ex5 [module, in RustExtraction.Test.RustExtractTests]
ex5.code [definition, in RustExtraction.Test.RustExtractTests]
ex5.test [definition, in RustExtraction.Test.RustExtractTests]
F
finish_print [definition, in RustExtraction.PrettyPrinterMonad]finish_print_lines [definition, in RustExtraction.PrettyPrinterMonad]
FixEnv [section, in RustExtraction.RustExtract]
FixEnv.print_term [section, in RustExtraction.RustExtract]
fresh [definition, in RustExtraction.RustExtract]
fresh_name [definition, in RustExtraction.PrettyPrinterMonad]
fresh_ty_arg_name [definition, in RustExtraction.RustExtract]
fresh_ident [definition, in RustExtraction.RustExtract]
G
get_current_line_length [definition, in RustExtraction.PrettyPrinterMonad]get_used_names [definition, in RustExtraction.PrettyPrinterMonad]
get_indent [definition, in RustExtraction.PrettyPrinterMonad]
get_num_inline_args [definition, in RustExtraction.RustExtract]
get_ind_ident [definition, in RustExtraction.RustExtract]
get_ty_const_ident [definition, in RustExtraction.RustExtract]
H
hex_of_Z [definition, in RustExtraction.StringExtra]hex_of_nat [definition, in RustExtraction.StringExtra]
hex_of_N [definition, in RustExtraction.StringExtra]
hex_of_positive [definition, in RustExtraction.StringExtra]
I
indent_stack [projection, in RustExtraction.PrettyPrinterMonad]indent_size [definition, in RustExtraction.RustExtract]
ind_attr_map [definition, in RustExtraction.RustExtract]
InternalFix [library]
is_letter [definition, in RustExtraction.StringExtra]
is_polymorphic [definition, in RustExtraction.RustExtract]
L
last_index_of [definition, in RustExtraction.StringExtra]lines [definition, in RustExtraction.StringExtra]
Loader [library]
lookup_ind_decl [definition, in RustExtraction.RustExtract]
lookup_mind [definition, in RustExtraction.RustExtract]
M
map_cur_output_line [definition, in RustExtraction.PrettyPrinterMonad]map_used_names [definition, in RustExtraction.PrettyPrinterMonad]
map_indent_stack [definition, in RustExtraction.PrettyPrinterMonad]
map_pps [definition, in RustExtraction.PrettyPrinterMonad]
min_needs_n_steps_nat [definition, in RustExtraction.Test.BernsteinYangTermination]
monad_append_concat [definition, in RustExtraction.PrettyPrinterMonad]
monad_append_join [definition, in RustExtraction.PrettyPrinterMonad]
Monad_PrettyPrinter [instance, in RustExtraction.PrettyPrinterMonad]
N
nat_syn_to_nat [definition, in RustExtraction.Common]nat_shiftl [definition, in RustExtraction.Test.BernsteinYangTermination]
needs_block [definition, in RustExtraction.RustExtract]
needs_n_steps [definition, in RustExtraction.Test.BernsteinYangTermination]
nl [definition, in RustExtraction.Common]
Nlog2up_nat [definition, in RustExtraction.StringExtra]
no_remaps [definition, in RustExtraction.Printing]
N_syn_to_nat [definition, in RustExtraction.Common]
O
odd [definition, in RustExtraction.Test.BernsteinYangTermination]odd [definition, in RustExtraction.Test.InternalFix]
optimize [definition, in RustExtraction.TopLevelFixes]
optimize_env [definition, in RustExtraction.TopLevelFixes]
optimize_decl [definition, in RustExtraction.TopLevelFixes]
optimize_aux [definition, in RustExtraction.TopLevelFixes]
output_lines [projection, in RustExtraction.PrettyPrinterMonad]
P
P [module, in RustExtraction.PrettyPrinterMonad]P [module, in RustExtraction.RustExtract]
parens [definition, in RustExtraction.Common]
parenthesize_ty_app_arg [definition, in RustExtraction.RustExtract]
parenthesize_case_discriminee [definition, in RustExtraction.RustExtract]
parenthesize_app_arg [definition, in RustExtraction.RustExtract]
parenthesize_app_head [definition, in RustExtraction.RustExtract]
PluginExtract [library]
plugin_extract_preamble [instance, in RustExtraction.PluginExtract]
pop_use [definition, in RustExtraction.PrettyPrinterMonad]
pop_indent [definition, in RustExtraction.PrettyPrinterMonad]
pos_syn_to_nat [definition, in RustExtraction.Common]
pos_syn_to_nat_aux [definition, in RustExtraction.Common]
Preamble [record, in RustExtraction.RustExtract]
prefix_spaces [definition, in RustExtraction.PrettyPrinterMonad]
PrettyPrinter [definition, in RustExtraction.PrettyPrinterMonad]
PrettyPrinterMonad [library]
PrettyPrinterState [record, in RustExtraction.PrettyPrinterMonad]
printer_fail [definition, in RustExtraction.PrettyPrinterMonad]
Printing [library]
print_list [definition, in RustExtraction.Common]
print_program [definition, in RustExtraction.RustExtract]
print_decls [definition, in RustExtraction.RustExtract]
print_decls_aux [definition, in RustExtraction.RustExtract]
print_type_alias [definition, in RustExtraction.RustExtract]
print_mutual_inductive_body [definition, in RustExtraction.RustExtract]
print_ind_ctor_definition [definition, in RustExtraction.RustExtract]
print_constant [definition, in RustExtraction.RustExtract]
print_term [definition, in RustExtraction.RustExtract]
print_remapped_case [definition, in RustExtraction.RustExtract]
print_case [definition, in RustExtraction.RustExtract]
print_const [definition, in RustExtraction.RustExtract]
print_constructor [definition, in RustExtraction.RustExtract]
print_app [definition, in RustExtraction.RustExtract]
print_type [definition, in RustExtraction.RustExtract]
print_type_aux [definition, in RustExtraction.RustExtract]
print_parenthesized_with [definition, in RustExtraction.RustExtract]
print_parenthesized [definition, in RustExtraction.RustExtract]
print_ind [definition, in RustExtraction.RustExtract]
print_full_names [projection, in RustExtraction.RustExtract]
program_preamble [projection, in RustExtraction.RustExtract]
PT [module, in RustExtraction.RustExtract]
push_use [definition, in RustExtraction.PrettyPrinterMonad]
push_indent [definition, in RustExtraction.PrettyPrinterMonad]
Q
quote_recursively_body [definition, in RustExtraction.Common]R
remap [definition, in RustExtraction.Common]remapped_inductive [record, in RustExtraction.Printing]
remaps [record, in RustExtraction.Printing]
remap_inline_constant [projection, in RustExtraction.Printing]
remap_constant [projection, in RustExtraction.Printing]
remap_inductive [projection, in RustExtraction.Printing]
remove_char [definition, in RustExtraction.StringExtra]
replace [definition, in RustExtraction.StringExtra]
replace_char [definition, in RustExtraction.StringExtra]
result_string_err [definition, in RustExtraction.PrettyPrinterMonad]
re_ind_match [projection, in RustExtraction.Printing]
re_ind_ctors [projection, in RustExtraction.Printing]
re_ind_name [projection, in RustExtraction.Printing]
RustConfig [instance, in RustExtraction.Test.RustExtractTests]
RustConfig [instance, in RustExtraction.PluginExtract]
RustExtract [library]
RustExtractTests [library]
RustPrintConfig [record, in RustExtraction.RustExtract]
S
SafeHead [module, in RustExtraction.Test.RustExtractTests]SafeHead.head_of_repeat_plus_one [definition, in RustExtraction.Test.RustExtractTests]
SafeHead.safe_head [definition, in RustExtraction.Test.RustExtractTests]
SafeHead.test [definition, in RustExtraction.Test.RustExtractTests]
shiftl [definition, in RustExtraction.Test.BernsteinYangTermination]
shiftr [definition, in RustExtraction.Test.BernsteinYangTermination]
starts_with [definition, in RustExtraction.StringExtra]
starts_with_cont [definition, in RustExtraction.StringExtra]
steps [definition, in RustExtraction.Test.BernsteinYangTermination]
StringExtra [library]
string_of_Z [definition, in RustExtraction.StringExtra]
string_of_positive [definition, in RustExtraction.StringExtra]
string_of_nat [definition, in RustExtraction.StringExtra]
string_of_N [definition, in RustExtraction.StringExtra]
string_of_list [definition, in RustExtraction.Common]
string_of_list_aux [definition, in RustExtraction.Common]
string_of_env_error [definition, in RustExtraction.PrettyPrinterMonad]
str_split [definition, in RustExtraction.StringExtra]
str_map [definition, in RustExtraction.StringExtra]
str_rev [definition, in RustExtraction.StringExtra]
substring_count [definition, in RustExtraction.StringExtra]
substring_from [definition, in RustExtraction.StringExtra]
s_to_bs [abbreviation, in RustExtraction.PrettyPrinterMonad]
s_to_bs [abbreviation, in RustExtraction.RustExtract]
T
T [module, in RustExtraction.RustExtract]T [module, in RustExtraction.PluginExtract]
term_box_symbol [projection, in RustExtraction.RustExtract]
TopLevelFixes [library]
top_preamble [projection, in RustExtraction.RustExtract]
to_lower [definition, in RustExtraction.StringExtra]
to_upper [definition, in RustExtraction.StringExtra]
to_globref [definition, in RustExtraction.Common]
transform [definition, in RustExtraction.TopLevelFixes]
TUtil [module, in RustExtraction.RustExtract]
type_box_symbol [projection, in RustExtraction.RustExtract]
ty_const_global_ident_of_kername [definition, in RustExtraction.RustExtract]
T2P [module, in RustExtraction.RustExtract]
U
uncapitalize [definition, in RustExtraction.StringExtra]used_names [projection, in RustExtraction.PrettyPrinterMonad]
W
W [definition, in RustExtraction.Test.BernsteinYangTermination]wrap_result [definition, in RustExtraction.PrettyPrinterMonad]
wrap_option [definition, in RustExtraction.PrettyPrinterMonad]
wrap_typing_result [definition, in RustExtraction.PrettyPrinterMonad]
wrap_EnvCheck [definition, in RustExtraction.PrettyPrinterMonad]
Z
Z_syn_to_Z [definition, in RustExtraction.Common]_
_Zneg [definition, in RustExtraction.Common]_Zpos [definition, in RustExtraction.Common]
_Z0 [definition, in RustExtraction.Common]
_Npos [definition, in RustExtraction.Common]
_N0 [definition, in RustExtraction.Common]
_xH [definition, in RustExtraction.Common]
_xO [definition, in RustExtraction.Common]
_xI [definition, in RustExtraction.Common]
other
<$ _ ; _ ; .. ; _ $> (string_scope) [notation, in RustExtraction.StringExtra]_ ^ _ [notation, in RustExtraction.RustExtract]
unfolded _ [notation, in RustExtraction.Common]
<! _ !> [notation, in RustExtraction.Common]
Notation Index
other
<$ _ ; _ ; .. ; _ $> (string_scope) [in RustExtraction.StringExtra]_ ^ _ [in RustExtraction.RustExtract]
unfolded _ [in RustExtraction.Common]
<! _ !> [in RustExtraction.Common]
Module Index
E
E [in RustExtraction.RustExtract]EF [in RustExtraction.RustExtract]
Ex [in RustExtraction.RustExtract]
ex1 [in RustExtraction.Test.RustExtractTests]
ex2 [in RustExtraction.Test.RustExtractTests]
ex3 [in RustExtraction.Test.RustExtractTests]
ex4 [in RustExtraction.Test.RustExtractTests]
ex5 [in RustExtraction.Test.RustExtractTests]
P
P [in RustExtraction.PrettyPrinterMonad]P [in RustExtraction.RustExtract]
PT [in RustExtraction.RustExtract]
S
SafeHead [in RustExtraction.Test.RustExtractTests]T
T [in RustExtraction.RustExtract]T [in RustExtraction.PluginExtract]
TUtil [in RustExtraction.RustExtract]
T2P [in RustExtraction.RustExtract]
Library Index
B
BernsteinYangTerminationC
CommonE
ExtractExtractionExtrRustBasic
ExtrRustCheckedArith
ExtrRustUncheckedArith
I
InternalFixL
LoaderP
PluginExtractPrettyPrinterMonad
Printing
R
RustExtractRustExtractTests
S
StringExtraT
TopLevelFixesProjection Index
A
any_type_symbol [in RustExtraction.RustExtract]C
cur_output_line [in RustExtraction.PrettyPrinterMonad]I
indent_stack [in RustExtraction.PrettyPrinterMonad]O
output_lines [in RustExtraction.PrettyPrinterMonad]P
print_full_names [in RustExtraction.RustExtract]program_preamble [in RustExtraction.RustExtract]
R
remap_inline_constant [in RustExtraction.Printing]remap_constant [in RustExtraction.Printing]
remap_inductive [in RustExtraction.Printing]
re_ind_match [in RustExtraction.Printing]
re_ind_ctors [in RustExtraction.Printing]
re_ind_name [in RustExtraction.Printing]
T
term_box_symbol [in RustExtraction.RustExtract]top_preamble [in RustExtraction.RustExtract]
type_box_symbol [in RustExtraction.RustExtract]
U
used_names [in RustExtraction.PrettyPrinterMonad]Instance Index
M
Monad_PrettyPrinter [in RustExtraction.PrettyPrinterMonad]P
plugin_extract_preamble [in RustExtraction.PluginExtract]R
RustConfig [in RustExtraction.Test.RustExtractTests]RustConfig [in RustExtraction.PluginExtract]
Section Index
F
FixEnv [in RustExtraction.RustExtract]FixEnv.print_term [in RustExtraction.RustExtract]
Abbreviation Index
B
bs_to_s [in RustExtraction.PrettyPrinterMonad]bs_to_s [in RustExtraction.RustExtract]
S
s_to_bs [in RustExtraction.PrettyPrinterMonad]s_to_bs [in RustExtraction.RustExtract]
Definition Index
A
ack [in RustExtraction.Test.InternalFix]append [in RustExtraction.PrettyPrinterMonad]
append_concat [in RustExtraction.PrettyPrinterMonad]
append_join [in RustExtraction.PrettyPrinterMonad]
append_nl [in RustExtraction.PrettyPrinterMonad]
C
capitalize [in RustExtraction.StringExtra]char_to_lower [in RustExtraction.StringExtra]
char_to_upper [in RustExtraction.StringExtra]
clean_local_ident [in RustExtraction.RustExtract]
clean_global_ident [in RustExtraction.RustExtract]
collect_output [in RustExtraction.PrettyPrinterMonad]
collect_output_lines [in RustExtraction.PrettyPrinterMonad]
const_global_ident_of_kername [in RustExtraction.RustExtract]
D
default_attrs [in RustExtraction.Test.RustExtractTests]default_attrs [in RustExtraction.PluginExtract]
divstep [in RustExtraction.Test.BernsteinYangTermination]
E
even [in RustExtraction.Test.InternalFix]even_odd [in RustExtraction.Test.InternalFix]
extract [in RustExtraction.Test.RustExtractTests]
extract [in RustExtraction.PluginExtract]
extract_def_name_exists [in RustExtraction.Common]
extract_rust_within_coq [in RustExtraction.RustExtract]
extract_lines [in RustExtraction.PluginExtract]
ex1.bar [in RustExtraction.Test.RustExtractTests]
ex1.ex1_test [in RustExtraction.Test.RustExtractTests]
ex1.foo [in RustExtraction.Test.RustExtractTests]
ex2.bar [in RustExtraction.Test.RustExtractTests]
ex2.ex2_test [in RustExtraction.Test.RustExtractTests]
ex2.foo [in RustExtraction.Test.RustExtractTests]
ex2.only_in_type [in RustExtraction.Test.RustExtractTests]
ex3.test [in RustExtraction.Test.RustExtractTests]
ex4.ack [in RustExtraction.Test.RustExtractTests]
ex4.test [in RustExtraction.Test.RustExtractTests]
ex5.code [in RustExtraction.Test.RustExtractTests]
ex5.test [in RustExtraction.Test.RustExtractTests]
F
finish_print [in RustExtraction.PrettyPrinterMonad]finish_print_lines [in RustExtraction.PrettyPrinterMonad]
fresh [in RustExtraction.RustExtract]
fresh_name [in RustExtraction.PrettyPrinterMonad]
fresh_ty_arg_name [in RustExtraction.RustExtract]
fresh_ident [in RustExtraction.RustExtract]
G
get_current_line_length [in RustExtraction.PrettyPrinterMonad]get_used_names [in RustExtraction.PrettyPrinterMonad]
get_indent [in RustExtraction.PrettyPrinterMonad]
get_num_inline_args [in RustExtraction.RustExtract]
get_ind_ident [in RustExtraction.RustExtract]
get_ty_const_ident [in RustExtraction.RustExtract]
H
hex_of_Z [in RustExtraction.StringExtra]hex_of_nat [in RustExtraction.StringExtra]
hex_of_N [in RustExtraction.StringExtra]
hex_of_positive [in RustExtraction.StringExtra]
I
indent_size [in RustExtraction.RustExtract]ind_attr_map [in RustExtraction.RustExtract]
is_letter [in RustExtraction.StringExtra]
is_polymorphic [in RustExtraction.RustExtract]
L
last_index_of [in RustExtraction.StringExtra]lines [in RustExtraction.StringExtra]
lookup_ind_decl [in RustExtraction.RustExtract]
lookup_mind [in RustExtraction.RustExtract]
M
map_cur_output_line [in RustExtraction.PrettyPrinterMonad]map_used_names [in RustExtraction.PrettyPrinterMonad]
map_indent_stack [in RustExtraction.PrettyPrinterMonad]
map_pps [in RustExtraction.PrettyPrinterMonad]
min_needs_n_steps_nat [in RustExtraction.Test.BernsteinYangTermination]
monad_append_concat [in RustExtraction.PrettyPrinterMonad]
monad_append_join [in RustExtraction.PrettyPrinterMonad]
N
nat_syn_to_nat [in RustExtraction.Common]nat_shiftl [in RustExtraction.Test.BernsteinYangTermination]
needs_block [in RustExtraction.RustExtract]
needs_n_steps [in RustExtraction.Test.BernsteinYangTermination]
nl [in RustExtraction.Common]
Nlog2up_nat [in RustExtraction.StringExtra]
no_remaps [in RustExtraction.Printing]
N_syn_to_nat [in RustExtraction.Common]
O
odd [in RustExtraction.Test.BernsteinYangTermination]odd [in RustExtraction.Test.InternalFix]
optimize [in RustExtraction.TopLevelFixes]
optimize_env [in RustExtraction.TopLevelFixes]
optimize_decl [in RustExtraction.TopLevelFixes]
optimize_aux [in RustExtraction.TopLevelFixes]
P
parens [in RustExtraction.Common]parenthesize_ty_app_arg [in RustExtraction.RustExtract]
parenthesize_case_discriminee [in RustExtraction.RustExtract]
parenthesize_app_arg [in RustExtraction.RustExtract]
parenthesize_app_head [in RustExtraction.RustExtract]
pop_use [in RustExtraction.PrettyPrinterMonad]
pop_indent [in RustExtraction.PrettyPrinterMonad]
pos_syn_to_nat [in RustExtraction.Common]
pos_syn_to_nat_aux [in RustExtraction.Common]
prefix_spaces [in RustExtraction.PrettyPrinterMonad]
PrettyPrinter [in RustExtraction.PrettyPrinterMonad]
printer_fail [in RustExtraction.PrettyPrinterMonad]
print_list [in RustExtraction.Common]
print_program [in RustExtraction.RustExtract]
print_decls [in RustExtraction.RustExtract]
print_decls_aux [in RustExtraction.RustExtract]
print_type_alias [in RustExtraction.RustExtract]
print_mutual_inductive_body [in RustExtraction.RustExtract]
print_ind_ctor_definition [in RustExtraction.RustExtract]
print_constant [in RustExtraction.RustExtract]
print_term [in RustExtraction.RustExtract]
print_remapped_case [in RustExtraction.RustExtract]
print_case [in RustExtraction.RustExtract]
print_const [in RustExtraction.RustExtract]
print_constructor [in RustExtraction.RustExtract]
print_app [in RustExtraction.RustExtract]
print_type [in RustExtraction.RustExtract]
print_type_aux [in RustExtraction.RustExtract]
print_parenthesized_with [in RustExtraction.RustExtract]
print_parenthesized [in RustExtraction.RustExtract]
print_ind [in RustExtraction.RustExtract]
push_use [in RustExtraction.PrettyPrinterMonad]
push_indent [in RustExtraction.PrettyPrinterMonad]
Q
quote_recursively_body [in RustExtraction.Common]R
remap [in RustExtraction.Common]remove_char [in RustExtraction.StringExtra]
replace [in RustExtraction.StringExtra]
replace_char [in RustExtraction.StringExtra]
result_string_err [in RustExtraction.PrettyPrinterMonad]
S
SafeHead.head_of_repeat_plus_one [in RustExtraction.Test.RustExtractTests]SafeHead.safe_head [in RustExtraction.Test.RustExtractTests]
SafeHead.test [in RustExtraction.Test.RustExtractTests]
shiftl [in RustExtraction.Test.BernsteinYangTermination]
shiftr [in RustExtraction.Test.BernsteinYangTermination]
starts_with [in RustExtraction.StringExtra]
starts_with_cont [in RustExtraction.StringExtra]
steps [in RustExtraction.Test.BernsteinYangTermination]
string_of_Z [in RustExtraction.StringExtra]
string_of_positive [in RustExtraction.StringExtra]
string_of_nat [in RustExtraction.StringExtra]
string_of_N [in RustExtraction.StringExtra]
string_of_list [in RustExtraction.Common]
string_of_list_aux [in RustExtraction.Common]
string_of_env_error [in RustExtraction.PrettyPrinterMonad]
str_split [in RustExtraction.StringExtra]
str_map [in RustExtraction.StringExtra]
str_rev [in RustExtraction.StringExtra]
substring_count [in RustExtraction.StringExtra]
substring_from [in RustExtraction.StringExtra]
T
to_lower [in RustExtraction.StringExtra]to_upper [in RustExtraction.StringExtra]
to_globref [in RustExtraction.Common]
transform [in RustExtraction.TopLevelFixes]
ty_const_global_ident_of_kername [in RustExtraction.RustExtract]
U
uncapitalize [in RustExtraction.StringExtra]W
W [in RustExtraction.Test.BernsteinYangTermination]wrap_result [in RustExtraction.PrettyPrinterMonad]
wrap_option [in RustExtraction.PrettyPrinterMonad]
wrap_typing_result [in RustExtraction.PrettyPrinterMonad]
wrap_EnvCheck [in RustExtraction.PrettyPrinterMonad]
Z
Z_syn_to_Z [in RustExtraction.Common]_
_Zneg [in RustExtraction.Common]_Zpos [in RustExtraction.Common]
_Z0 [in RustExtraction.Common]
_Npos [in RustExtraction.Common]
_N0 [in RustExtraction.Common]
_xH [in RustExtraction.Common]
_xO [in RustExtraction.Common]
_xI [in RustExtraction.Common]
Record Index
P
Preamble [in RustExtraction.RustExtract]PrettyPrinterState [in RustExtraction.PrettyPrinterMonad]
R
remapped_inductive [in RustExtraction.Printing]remaps [in RustExtraction.Printing]
RustPrintConfig [in RustExtraction.RustExtract]
| 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 | (225 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 | (4 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 | (16 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 | (15 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 | (16 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 | (4 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 | (2 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 | (4 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 | (159 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 | (5 entries) |