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 | (471 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 | (12 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 | (43 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 | (6 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 | (22 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 | (10 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 | (4 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 | (31 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 | (6 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 | (7 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 | (3 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 | (316 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 | (11 entries) |
Global Index
A
ack [definition, in TypedExtraction.Tests.InternalFix]ack [definition, in TypedExtraction.Tests.Ack]
Ack [library]
Add [constructor, in TypedExtraction.Tests.ElmForms]
any_type_symbol [projection, in TypedExtraction.Rust.RustExtract]
any_type_symbol [projection, in TypedExtraction.Elm.ElmExtract]
append [definition, in TypedExtraction.Common.PrettyPrinterMonad]
append_concat [definition, in TypedExtraction.Common.PrettyPrinterMonad]
append_join [definition, in TypedExtraction.Common.PrettyPrinterMonad]
append_nl [definition, in TypedExtraction.Common.PrettyPrinterMonad]
aRelevant [definition, in TypedExtraction.Tests.RecordSet]
B
BernsteinYangTermination [library]C
capitalize [definition, in TypedExtraction.Common.StringExtra]char_to_lower [definition, in TypedExtraction.Common.StringExtra]
char_to_upper [definition, in TypedExtraction.Common.StringExtra]
clean_local_ident [definition, in TypedExtraction.Rust.RustExtract]
clean_global_ident [definition, in TypedExtraction.Rust.RustExtract]
Cmd [inductive, in TypedExtraction.Tests.ElmForms]
Cmd_sind [definition, in TypedExtraction.Tests.ElmForms]
Cmd_rec [definition, in TypedExtraction.Tests.ElmForms]
Cmd_ind [definition, in TypedExtraction.Tests.ElmForms]
Cmd_rect [definition, in TypedExtraction.Tests.ElmForms]
collect_output [definition, in TypedExtraction.Common.PrettyPrinterMonad]
collect_output_lines [definition, in TypedExtraction.Common.PrettyPrinterMonad]
Common [library]
const_global_ident_of_kername [definition, in TypedExtraction.Rust.RustExtract]
currentEntry [projection, in TypedExtraction.Tests.ElmForms]
cur_output_line [projection, in TypedExtraction.Common.PrettyPrinterMonad]
D
default_attrs [definition, in TypedExtraction.Rust.PluginExtract]default_attrs [definition, in TypedExtraction.Tests.RustExtractTests]
divstep [definition, in TypedExtraction.Tests.BernsteinYangTermination]
E
E [module, in TypedExtraction.Rust.RustExtract]E [module, in TypedExtraction.Elm.ElmExtract]
EF [module, in TypedExtraction.Rust.RustExtract]
EF [module, in TypedExtraction.Elm.ElmExtract]
ElmBoxes [instance, in TypedExtraction.Tests.ElmForms]
ElmBoxes [instance, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples [module, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.ackermann [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmExamples_nth [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_foldl [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_map [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.head_of_repeat_plus_one [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.inc_counter [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.main_and_test [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.Preambule [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.result_foldl [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.result_map [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.result_nth [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_head [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_partial [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_full [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred [definition, in TypedExtraction.Tests.ElmExtractExamples]
ElmExtract [library]
ElmExtractExamples [library]
ElmExtractTests [library]
ElmForms [library]
elmmd_extract [projection, in TypedExtraction.Tests.ElmForms]
ElmMod [record, in TypedExtraction.Tests.ElmForms]
ElmPrintConfig [record, in TypedExtraction.Elm.ElmExtract]
elm_extraction [definition, in TypedExtraction.Tests.ElmForms]
elm_false_rec [definition, in TypedExtraction.Elm.ElmExtract]
emptyNameError [definition, in TypedExtraction.Tests.ElmForms]
Entry [record, in TypedExtraction.Tests.ElmForms]
errors [projection, in TypedExtraction.Tests.ElmForms]
even [definition, in TypedExtraction.Tests.InternalFix]
even_odd [definition, in TypedExtraction.Tests.InternalFix]
Ex [module, in TypedExtraction.Rust.RustExtract]
Ex [module, in TypedExtraction.Elm.ElmExtract]
extract [definition, in TypedExtraction.Rust.PluginExtract]
extract [definition, in TypedExtraction.Tests.RustExtractTests]
extract [definition, in TypedExtraction.Tests.ElmExtractTests]
ExtractExtraction [library]
extract_def_name_exists [definition, in TypedExtraction.Common.Common]
extract_def_name [definition, in TypedExtraction.Common.Common]
extract_lines [definition, in TypedExtraction.Rust.PluginExtract]
extract_elm_within_rocq [definition, in TypedExtraction.Tests.ElmForms]
extract_rust_within_rocq [definition, in TypedExtraction.Rust.RustExtract]
ExtrRustBasic [library]
ExtrRustCheckedArith [library]
ExtrRustUncheckedArith [library]
ex_infix1.test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex_infix1.TT [definition, in TypedExtraction.Tests.ElmExtractTests]
ex_infix1 [module, in TypedExtraction.Tests.ElmExtractTests]
ex1 [module, in TypedExtraction.Tests.RustExtractTests]
ex1 [module, in TypedExtraction.Tests.ElmExtractTests]
ex1.bar [definition, in TypedExtraction.Tests.RustExtractTests]
ex1.bar [definition, in TypedExtraction.Tests.ElmExtractTests]
ex1.ex1_test [definition, in TypedExtraction.Tests.RustExtractTests]
ex1.ex1_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex1.foo [definition, in TypedExtraction.Tests.RustExtractTests]
ex1.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex10 [module, in TypedExtraction.Tests.ElmExtractTests]
ex10.ex10_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex10.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex11 [module, in TypedExtraction.Tests.ElmExtractTests]
ex11.Monad_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex12 [module, in TypedExtraction.Tests.ElmExtractTests]
ex12.idT [definition, in TypedExtraction.Tests.ElmExtractTests]
ex12.test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex12.weird_id [definition, in TypedExtraction.Tests.ElmExtractTests]
ex13 [module, in TypedExtraction.Tests.ElmExtractTests]
ex13.opt [definition, in TypedExtraction.Tests.ElmExtractTests]
ex13.test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex13.unwrap [definition, in TypedExtraction.Tests.ElmExtractTests]
ex2 [module, in TypedExtraction.Tests.RustExtractTests]
ex2 [module, in TypedExtraction.Tests.ElmExtractTests]
ex2.bar [definition, in TypedExtraction.Tests.RustExtractTests]
ex2.bar [definition, in TypedExtraction.Tests.ElmExtractTests]
ex2.ex2_test [definition, in TypedExtraction.Tests.RustExtractTests]
ex2.ex2_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex2.foo [definition, in TypedExtraction.Tests.RustExtractTests]
ex2.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex2.only_in_type [definition, in TypedExtraction.Tests.RustExtractTests]
ex2.only_in_type [definition, in TypedExtraction.Tests.ElmExtractTests]
ex3 [module, in TypedExtraction.Tests.RustExtractTests]
ex3 [module, in TypedExtraction.Tests.ElmExtractTests]
ex3.bar [definition, in TypedExtraction.Tests.ElmExtractTests]
ex3.baz [definition, in TypedExtraction.Tests.ElmExtractTests]
ex3.ex3_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex3.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex3.test [definition, in TypedExtraction.Tests.RustExtractTests]
ex4 [module, in TypedExtraction.Tests.RustExtractTests]
ex4 [module, in TypedExtraction.Tests.ElmExtractTests]
ex4.ack [definition, in TypedExtraction.Tests.RustExtractTests]
ex4.ex4_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex4.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex4.test [definition, in TypedExtraction.Tests.RustExtractTests]
ex5 [module, in TypedExtraction.Tests.RustExtractTests]
ex5 [module, in TypedExtraction.Tests.ElmExtractTests]
ex5.code [definition, in TypedExtraction.Tests.RustExtractTests]
ex5.ex5_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex5.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex5.test [definition, in TypedExtraction.Tests.RustExtractTests]
ex6 [module, in TypedExtraction.Tests.ElmExtractTests]
ex6.bar [definition, in TypedExtraction.Tests.ElmExtractTests]
ex6.baz [definition, in TypedExtraction.Tests.ElmExtractTests]
ex6.ex6_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex6.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex7 [module, in TypedExtraction.Tests.ElmExtractTests]
ex7.bar [definition, in TypedExtraction.Tests.ElmExtractTests]
ex7.ex7_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex7.foo [definition, in TypedExtraction.Tests.ElmExtractTests]
ex8 [module, in TypedExtraction.Tests.ElmExtractTests]
ex8.ex8_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd [inductive, in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_sind [definition, in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rec [definition, in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_ind [definition, in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rect [definition, in TypedExtraction.Tests.ElmExtractTests]
ex8.MPIConstr [constructor, in TypedExtraction.Tests.ElmExtractTests]
ex9 [module, in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity [inductive, in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_test [definition, in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_sind [definition, in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rec [definition, in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_ind [definition, in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rect [definition, in TypedExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr1 [constructor, in TypedExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr2 [constructor, in TypedExtraction.Tests.ElmExtractTests]
F
false_elim_def [projection, in TypedExtraction.Elm.ElmExtract]finish_print [definition, in TypedExtraction.Common.PrettyPrinterMonad]
finish_print_lines [definition, in TypedExtraction.Common.PrettyPrinterMonad]
FixEnv [section, in TypedExtraction.Rust.RustExtract]
FixEnv [section, in TypedExtraction.Elm.ElmExtract]
FixEnv.ind_attrs [variable, in TypedExtraction.Rust.RustExtract]
FixEnv.print_term.print_term [variable, in TypedExtraction.Rust.RustExtract]
FixEnv.print_term [section, in TypedExtraction.Rust.RustExtract]
FixEnv.remaps [variable, in TypedExtraction.Rust.RustExtract]
FixEnv.translate [variable, in TypedExtraction.Elm.ElmExtract]
_ ^ _ [notation, in TypedExtraction.Elm.ElmExtract]
FixEnv.Σ [variable, in TypedExtraction.Rust.RustExtract]
FixEnv.Σ [variable, in TypedExtraction.Elm.ElmExtract]
fresh [definition, in TypedExtraction.Rust.RustExtract]
fresh [definition, in TypedExtraction.Elm.ElmExtract]
fresh_name [definition, in TypedExtraction.Common.PrettyPrinterMonad]
fresh_ty_arg_name [definition, in TypedExtraction.Rust.RustExtract]
fresh_ident [definition, in TypedExtraction.Rust.RustExtract]
fresh_ty_arg_name [definition, in TypedExtraction.Elm.ElmExtract]
fresh_ident [definition, in TypedExtraction.Elm.ElmExtract]
G
general_wrapped [definition, in TypedExtraction.Tests.ElmForms]general_extract [definition, in TypedExtraction.Tests.ElmExtractTests]
general_wrapped [definition, in TypedExtraction.Tests.ElmExtractExamples]
get_current_line_length [definition, in TypedExtraction.Common.PrettyPrinterMonad]
get_used_names [definition, in TypedExtraction.Common.PrettyPrinterMonad]
get_indent [definition, in TypedExtraction.Common.PrettyPrinterMonad]
get_num_inline_args [definition, in TypedExtraction.Rust.RustExtract]
get_ind_ident [definition, in TypedExtraction.Rust.RustExtract]
get_ty_const_ident [definition, in TypedExtraction.Rust.RustExtract]
get_infix [definition, in TypedExtraction.Elm.ElmExtract]
get_ty_arg_name [definition, in TypedExtraction.Elm.ElmExtract]
get_ident_name [definition, in TypedExtraction.Elm.ElmExtract]
get_ctor_name [definition, in TypedExtraction.Elm.ElmExtract]
get_ty_name [definition, in TypedExtraction.Elm.ElmExtract]
get_fun_name [definition, in TypedExtraction.Elm.ElmExtract]
H
header_and_imports [definition, in TypedExtraction.Tests.ElmForms]hex_of_Z [definition, in TypedExtraction.Common.StringExtra]
hex_of_nat [definition, in TypedExtraction.Common.StringExtra]
hex_of_N [definition, in TypedExtraction.Common.StringExtra]
hex_of_positive [definition, in TypedExtraction.Common.StringExtra]
I
indent_stack [projection, in TypedExtraction.Common.PrettyPrinterMonad]indent_size [definition, in TypedExtraction.Rust.RustExtract]
indent_size [definition, in TypedExtraction.Elm.ElmExtract]
ind_attr_map [definition, in TypedExtraction.Rust.RustExtract]
initModel [definition, in TypedExtraction.Tests.ElmForms]
InternalFix [library]
is_letter [definition, in TypedExtraction.Common.StringExtra]
is_polymorphic [definition, in TypedExtraction.Rust.RustExtract]
L
last_index_of [definition, in TypedExtraction.Common.StringExtra]lexicographic_ordering_wf [lemma, in TypedExtraction.Tests.Ack]
lexicographic_ordering [definition, in TypedExtraction.Tests.Ack]
lines [definition, in TypedExtraction.Common.StringExtra]
Loader [library]
lookup_ind_decl [definition, in TypedExtraction.Rust.RustExtract]
lookup_mind [definition, in TypedExtraction.Rust.RustExtract]
lookup_ind_decl [definition, in TypedExtraction.Elm.ElmExtract]
lookup_mind [definition, in TypedExtraction.Elm.ElmExtract]
lt_wf_double_ind [lemma, in TypedExtraction.Tests.Ack]
lt_wf_ind [lemma, in TypedExtraction.Tests.Ack]
M
make_setters [definition, in TypedExtraction.Tests.RecordSet]map_cur_output_line [definition, in TypedExtraction.Common.PrettyPrinterMonad]
map_used_names [definition, in TypedExtraction.Common.PrettyPrinterMonad]
map_indent_stack [definition, in TypedExtraction.Common.PrettyPrinterMonad]
map_pps [definition, in TypedExtraction.Common.PrettyPrinterMonad]
min_needs_n_steps_nat [definition, in TypedExtraction.Tests.BernsteinYangTermination]
Model [record, in TypedExtraction.Tests.ElmForms]
monad_append_concat [definition, in TypedExtraction.Common.PrettyPrinterMonad]
monad_append_join [definition, in TypedExtraction.Common.PrettyPrinterMonad]
Monad_PrettyPrinter [instance, in TypedExtraction.Common.PrettyPrinterMonad]
Msg [inductive, in TypedExtraction.Tests.ElmForms]
MsgName [constructor, in TypedExtraction.Tests.ElmForms]
MsgPassword [constructor, in TypedExtraction.Tests.ElmForms]
MsgPasswordAgain [constructor, in TypedExtraction.Tests.ElmForms]
Msg_sind [definition, in TypedExtraction.Tests.ElmForms]
Msg_rec [definition, in TypedExtraction.Tests.ElmForms]
Msg_ind [definition, in TypedExtraction.Tests.ElmForms]
Msg_rect [definition, in TypedExtraction.Tests.ElmForms]
N
name [projection, in TypedExtraction.Tests.ElmForms]nat_syn_to_nat [definition, in TypedExtraction.Common.Common]
nat_shiftl [definition, in TypedExtraction.Tests.BernsteinYangTermination]
needs_block [definition, in TypedExtraction.Rust.RustExtract]
needs_n_steps [definition, in TypedExtraction.Tests.BernsteinYangTermination]
nl [definition, in TypedExtraction.Common.Common]
Nlog2up_nat [definition, in TypedExtraction.Common.StringExtra]
none [constructor, in TypedExtraction.Tests.ElmForms]
nonEmptyString [definition, in TypedExtraction.Tests.ElmForms]
no_remaps [definition, in TypedExtraction.Rust.Printing]
no_check_args [definition, in TypedExtraction.Tests.ElmExtractTests]
no_check_args [definition, in TypedExtraction.Tests.ElmExtractExamples]
N_syn_to_nat [definition, in TypedExtraction.Common.Common]
O
odd [definition, in TypedExtraction.Tests.InternalFix]odd [definition, in TypedExtraction.Tests.BernsteinYangTermination]
optimize [definition, in TypedExtraction.Rust.TopLevelFixes]
optimize_env [definition, in TypedExtraction.Rust.TopLevelFixes]
optimize_decl [definition, in TypedExtraction.Rust.TopLevelFixes]
optimize_aux [definition, in TypedExtraction.Rust.TopLevelFixes]
output_lines [projection, in TypedExtraction.Common.PrettyPrinterMonad]
P
P [module, in TypedExtraction.Common.PrettyPrinterMonad]P [module, in TypedExtraction.Rust.RustExtract]
P [module, in TypedExtraction.Elm.ElmExtract]
parens [definition, in TypedExtraction.Common.Common]
parenthesize_ty_app_arg [definition, in TypedExtraction.Rust.RustExtract]
parenthesize_case_discriminee [definition, in TypedExtraction.Rust.RustExtract]
parenthesize_app_arg [definition, in TypedExtraction.Rust.RustExtract]
parenthesize_app_head [definition, in TypedExtraction.Rust.RustExtract]
parenthesize_ind_ctor_ty [definition, in TypedExtraction.Elm.ElmExtract]
parenthesize_ty_app_arg [definition, in TypedExtraction.Elm.ElmExtract]
parenthesize_prod_domain [definition, in TypedExtraction.Elm.ElmExtract]
parenthesize_case_branch [definition, in TypedExtraction.Elm.ElmExtract]
parenthesize_case_discriminee [definition, in TypedExtraction.Elm.ElmExtract]
parenthesize_app_arg [definition, in TypedExtraction.Elm.ElmExtract]
parenthesize_app_head [definition, in TypedExtraction.Elm.ElmExtract]
password [projection, in TypedExtraction.Tests.ElmForms]
passwordAgain [projection, in TypedExtraction.Tests.ElmForms]
passwordIsTooShortError [definition, in TypedExtraction.Tests.ElmForms]
passwordsDoNotMatchError [definition, in TypedExtraction.Tests.ElmForms]
PluginExtract [library]
plugin_extract_preamble [instance, in TypedExtraction.Rust.PluginExtract]
pop_use [definition, in TypedExtraction.Common.PrettyPrinterMonad]
pop_indent [definition, in TypedExtraction.Common.PrettyPrinterMonad]
pos_syn_to_nat [definition, in TypedExtraction.Common.Common]
pos_syn_to_nat_aux [definition, in TypedExtraction.Common.Common]
preamble [definition, in TypedExtraction.Tests.ElmForms]
Preamble [record, in TypedExtraction.Rust.RustExtract]
prefix_spaces [definition, in TypedExtraction.Common.PrettyPrinterMonad]
PrettyPrinter [definition, in TypedExtraction.Common.PrettyPrinterMonad]
PrettyPrinterMonad [library]
PrettyPrinterState [record, in TypedExtraction.Common.PrettyPrinterMonad]
printer_fail [definition, in TypedExtraction.Common.PrettyPrinterMonad]
Printing [library]
print_list [definition, in TypedExtraction.Common.Common]
print_program [definition, in TypedExtraction.Rust.RustExtract]
print_decls [definition, in TypedExtraction.Rust.RustExtract]
print_decls_aux [definition, in TypedExtraction.Rust.RustExtract]
print_type_alias [definition, in TypedExtraction.Rust.RustExtract]
print_mutual_inductive_body [definition, in TypedExtraction.Rust.RustExtract]
print_ind_ctor_definition [definition, in TypedExtraction.Rust.RustExtract]
print_constant [definition, in TypedExtraction.Rust.RustExtract]
print_term [definition, in TypedExtraction.Rust.RustExtract]
print_remapped_case [definition, in TypedExtraction.Rust.RustExtract]
print_case [definition, in TypedExtraction.Rust.RustExtract]
print_const [definition, in TypedExtraction.Rust.RustExtract]
print_constructor [definition, in TypedExtraction.Rust.RustExtract]
print_app [definition, in TypedExtraction.Rust.RustExtract]
print_type [definition, in TypedExtraction.Rust.RustExtract]
print_type_aux [definition, in TypedExtraction.Rust.RustExtract]
print_parenthesized_with [definition, in TypedExtraction.Rust.RustExtract]
print_parenthesized [definition, in TypedExtraction.Rust.RustExtract]
print_ind [definition, in TypedExtraction.Rust.RustExtract]
print_full_names [projection, in TypedExtraction.Rust.RustExtract]
print_env [definition, in TypedExtraction.Elm.ElmExtract]
print_type_alias [definition, in TypedExtraction.Elm.ElmExtract]
print_mutual_inductive_body [definition, in TypedExtraction.Elm.ElmExtract]
print_ind_ctor_definition [definition, in TypedExtraction.Elm.ElmExtract]
print_constant [definition, in TypedExtraction.Elm.ElmExtract]
print_term [definition, in TypedExtraction.Elm.ElmExtract]
print_infix_match_branch [definition, in TypedExtraction.Elm.ElmExtract]
print_define_term [definition, in TypedExtraction.Elm.ElmExtract]
print_type [definition, in TypedExtraction.Elm.ElmExtract]
print_parenthesized [definition, in TypedExtraction.Elm.ElmExtract]
print_ind_ctor [definition, in TypedExtraction.Elm.ElmExtract]
print_ind [definition, in TypedExtraction.Elm.ElmExtract]
print_full_names [projection, in TypedExtraction.Elm.ElmExtract]
program_preamble [projection, in TypedExtraction.Rust.RustExtract]
PT [module, in TypedExtraction.Rust.RustExtract]
PT [module, in TypedExtraction.Elm.ElmExtract]
push_use [definition, in TypedExtraction.Common.PrettyPrinterMonad]
push_indent [definition, in TypedExtraction.Common.PrettyPrinterMonad]
Q
quote_recursively_body [definition, in TypedExtraction.Common.Common]R
RecordSet [library]RecordSetNotations [module, in TypedExtraction.Tests.RecordSet]
_ <| _ := _ |> (record_set) [notation, in TypedExtraction.Tests.RecordSet]
_ <| _ ::= _ |> (record_set) [notation, in TypedExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ := _ |> [notation, in TypedExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ ::= _ |> [notation, in TypedExtraction.Tests.RecordSet]
RecordUpdate [library]
recursor_ex.ex_test [definition, in TypedExtraction.Tests.ElmExtractTests]
recursor_ex.test_is_map [lemma, in TypedExtraction.Tests.ElmExtractTests]
recursor_ex.test [definition, in TypedExtraction.Tests.ElmExtractTests]
recursor_ex [module, in TypedExtraction.Tests.ElmExtractTests]
remap [definition, in TypedExtraction.Common.Common]
remapped_inductive [record, in TypedExtraction.Rust.Printing]
remaps [record, in TypedExtraction.Rust.Printing]
remap_inline_constant [projection, in TypedExtraction.Rust.Printing]
remap_constant [projection, in TypedExtraction.Rust.Printing]
remap_inductive [projection, in TypedExtraction.Rust.Printing]
remove_char [definition, in TypedExtraction.Common.StringExtra]
replace [definition, in TypedExtraction.Common.StringExtra]
replace_char [definition, in TypedExtraction.Common.StringExtra]
result_of_option [definition, in TypedExtraction.Common.Common]
result_of_typing_result [definition, in TypedExtraction.Common.Common]
result_string_err [definition, in TypedExtraction.Common.PrettyPrinterMonad]
result_bytestring_err [definition, in TypedExtraction.Tests.ElmExtractTests]
result_err_bytestring [definition, in TypedExtraction.Tests.ElmExtractExamples]
re_ind_match [projection, in TypedExtraction.Rust.Printing]
re_ind_ctors [projection, in TypedExtraction.Rust.Printing]
re_ind_name [projection, in TypedExtraction.Rust.Printing]
RustConfig [instance, in TypedExtraction.Rust.PluginExtract]
RustConfig [instance, in TypedExtraction.Tests.RustExtractTests]
RustExtract [library]
RustExtractTests [library]
RustPrintConfig [record, in TypedExtraction.Rust.RustExtract]
S
SafeHead [module, in TypedExtraction.Tests.RustExtractTests]SafeHead.head_of_repeat_plus_one [definition, in TypedExtraction.Tests.RustExtractTests]
SafeHead.safe_head [definition, in TypedExtraction.Tests.RustExtractTests]
SafeHead.test [definition, in TypedExtraction.Tests.RustExtractTests]
seName [projection, in TypedExtraction.Tests.ElmForms]
seNames [definition, in TypedExtraction.Tests.ElmForms]
sePassword [projection, in TypedExtraction.Tests.ElmForms]
SetterFromGetter [record, in TypedExtraction.Tests.RecordSet]
SetterFromGetter [inductive, in TypedExtraction.Tests.RecordSet]
setter_from_getter [projection, in TypedExtraction.Tests.RecordSet]
setter_from_getter [constructor, in TypedExtraction.Tests.RecordSet]
shiftl [definition, in TypedExtraction.Tests.BernsteinYangTermination]
shiftr [definition, in TypedExtraction.Tests.BernsteinYangTermination]
StandardBoxes [instance, in TypedExtraction.Tests.ElmExtractTests]
starts_with [definition, in TypedExtraction.Common.StringExtra]
starts_with_cont [definition, in TypedExtraction.Common.StringExtra]
steps [definition, in TypedExtraction.Tests.BernsteinYangTermination]
StorageMsg [inductive, in TypedExtraction.Tests.ElmForms]
StorageMsg_sind [definition, in TypedExtraction.Tests.ElmForms]
StorageMsg_rec [definition, in TypedExtraction.Tests.ElmForms]
StorageMsg_ind [definition, in TypedExtraction.Tests.ElmForms]
StorageMsg_rect [definition, in TypedExtraction.Tests.ElmForms]
StoredEntry [record, in TypedExtraction.Tests.ElmForms]
StringExtra [library]
string_of_list [definition, in TypedExtraction.Common.Common]
string_of_list_aux [definition, in TypedExtraction.Common.Common]
string_of_env_error [definition, in TypedExtraction.Common.Common]
string_of_env_error [definition, in TypedExtraction.Common.PrettyPrinterMonad]
string_of_Z [definition, in TypedExtraction.Common.StringExtra]
string_of_positive [definition, in TypedExtraction.Common.StringExtra]
string_of_nat [definition, in TypedExtraction.Common.StringExtra]
string_of_N [definition, in TypedExtraction.Common.StringExtra]
str_split [definition, in TypedExtraction.Common.StringExtra]
str_map [definition, in TypedExtraction.Common.StringExtra]
str_rev [definition, in TypedExtraction.Common.StringExtra]
substring_count [definition, in TypedExtraction.Common.StringExtra]
substring_from [definition, in TypedExtraction.Common.StringExtra]
T
T [module, in TypedExtraction.Rust.PluginExtract]T [module, in TypedExtraction.Rust.RustExtract]
T [module, in TypedExtraction.Elm.ElmExtract]
term_box_symbol [projection, in TypedExtraction.Rust.RustExtract]
term_box_symbol [projection, in TypedExtraction.Elm.ElmExtract]
TopLevelFixes [library]
top_preamble [projection, in TypedExtraction.Rust.RustExtract]
toValidStoredEntry [definition, in TypedExtraction.Tests.ElmForms]
to_string_name [definition, in TypedExtraction.Common.Common]
to_globref [definition, in TypedExtraction.Common.Common]
to_kername [definition, in TypedExtraction.Common.Common]
to_inline [definition, in TypedExtraction.Tests.ElmForms]
to_lower [definition, in TypedExtraction.Common.StringExtra]
to_upper [definition, in TypedExtraction.Common.StringExtra]
transform [definition, in TypedExtraction.Rust.TopLevelFixes]
TT [definition, in TypedExtraction.Tests.ElmForms]
TUtil [module, in TypedExtraction.Rust.RustExtract]
TUtil [module, in TypedExtraction.Elm.ElmExtract]
type_box_symbol [projection, in TypedExtraction.Rust.RustExtract]
type_box_symbol [projection, in TypedExtraction.Elm.ElmExtract]
type_scheme_ex.singleton_vec_test [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.singleton_vec [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.vec [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied_test [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_test [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3 [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.P [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample [module, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple_test [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow_test [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.general_extract_tc [definition, in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex [module, in TypedExtraction.Tests.ElmExtractTests]
ty_const_global_ident_of_kername [definition, in TypedExtraction.Rust.RustExtract]
T2P [module, in TypedExtraction.Rust.RustExtract]
T2P [module, in TypedExtraction.Elm.ElmExtract]
U
uncapitalize [definition, in TypedExtraction.Common.StringExtra]UpdateEntry [constructor, in TypedExtraction.Tests.ElmForms]
updateEntry [definition, in TypedExtraction.Tests.ElmForms]
updateModel [definition, in TypedExtraction.Tests.ElmForms]
used_names [projection, in TypedExtraction.Common.PrettyPrinterMonad]
userAlreadyExistsError [definition, in TypedExtraction.Tests.ElmForms]
users [projection, in TypedExtraction.Tests.ElmForms]
USER_FORM_APP [definition, in TypedExtraction.Tests.ElmForms]
V
validateModel [definition, in TypedExtraction.Tests.ElmForms]ValidEntry [definition, in TypedExtraction.Tests.ElmForms]
validPassword [definition, in TypedExtraction.Tests.ElmForms]
ValidStoredEntry [definition, in TypedExtraction.Tests.ElmForms]
W
W [definition, in TypedExtraction.Tests.BernsteinYangTermination]wrapped [definition, in TypedExtraction.Tests.ElmExtractExamples]
wrap_result [definition, in TypedExtraction.Common.PrettyPrinterMonad]
wrap_option [definition, in TypedExtraction.Common.PrettyPrinterMonad]
wrap_typing_result [definition, in TypedExtraction.Common.PrettyPrinterMonad]
wrap_EnvCheck [definition, in TypedExtraction.Common.PrettyPrinterMonad]
Z
Z_syn_to_Z [definition, in TypedExtraction.Common.Common]_
_Zneg [definition, in TypedExtraction.Common.Common]_Zpos [definition, in TypedExtraction.Common.Common]
_Z0 [definition, in TypedExtraction.Common.Common]
_Npos [definition, in TypedExtraction.Common.Common]
_N0 [definition, in TypedExtraction.Common.Common]
_xH [definition, in TypedExtraction.Common.Common]
_xO [definition, in TypedExtraction.Common.Common]
_xI [definition, in TypedExtraction.Common.Common]
other
<$ _ ; _ ; .. ; _ $> (bs_scope) [notation, in TypedExtraction.Common.StringExtra]string_literal _ (string_scope) [notation, in TypedExtraction.Tests.ElmForms]
_ ^ _ [notation, in TypedExtraction.Rust.RustExtract]
remap_ctor _ of _ to _ [notation, in TypedExtraction.Tests.ElmForms]
unfolded _ [notation, in TypedExtraction.Common.Common]
<! _ !> [notation, in TypedExtraction.Common.Common]
<%% _ %%> [notation, in TypedExtraction.Common.Common]
Notation Index
F
_ ^ _ [in TypedExtraction.Elm.ElmExtract]R
_ <| _ := _ |> (record_set) [in TypedExtraction.Tests.RecordSet]_ <| _ ::= _ |> (record_set) [in TypedExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ := _ |> [in TypedExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ ::= _ |> [in TypedExtraction.Tests.RecordSet]
other
<$ _ ; _ ; .. ; _ $> (bs_scope) [in TypedExtraction.Common.StringExtra]string_literal _ (string_scope) [in TypedExtraction.Tests.ElmForms]
_ ^ _ [in TypedExtraction.Rust.RustExtract]
remap_ctor _ of _ to _ [in TypedExtraction.Tests.ElmForms]
unfolded _ [in TypedExtraction.Common.Common]
<! _ !> [in TypedExtraction.Common.Common]
<%% _ %%> [in TypedExtraction.Common.Common]
Module Index
E
E [in TypedExtraction.Rust.RustExtract]E [in TypedExtraction.Elm.ElmExtract]
EF [in TypedExtraction.Rust.RustExtract]
EF [in TypedExtraction.Elm.ElmExtract]
ElmExamples [in TypedExtraction.Tests.ElmExtractExamples]
Ex [in TypedExtraction.Rust.RustExtract]
Ex [in TypedExtraction.Elm.ElmExtract]
ex_infix1 [in TypedExtraction.Tests.ElmExtractTests]
ex1 [in TypedExtraction.Tests.RustExtractTests]
ex1 [in TypedExtraction.Tests.ElmExtractTests]
ex10 [in TypedExtraction.Tests.ElmExtractTests]
ex11 [in TypedExtraction.Tests.ElmExtractTests]
ex12 [in TypedExtraction.Tests.ElmExtractTests]
ex13 [in TypedExtraction.Tests.ElmExtractTests]
ex2 [in TypedExtraction.Tests.RustExtractTests]
ex2 [in TypedExtraction.Tests.ElmExtractTests]
ex3 [in TypedExtraction.Tests.RustExtractTests]
ex3 [in TypedExtraction.Tests.ElmExtractTests]
ex4 [in TypedExtraction.Tests.RustExtractTests]
ex4 [in TypedExtraction.Tests.ElmExtractTests]
ex5 [in TypedExtraction.Tests.RustExtractTests]
ex5 [in TypedExtraction.Tests.ElmExtractTests]
ex6 [in TypedExtraction.Tests.ElmExtractTests]
ex7 [in TypedExtraction.Tests.ElmExtractTests]
ex8 [in TypedExtraction.Tests.ElmExtractTests]
ex9 [in TypedExtraction.Tests.ElmExtractTests]
P
P [in TypedExtraction.Common.PrettyPrinterMonad]P [in TypedExtraction.Rust.RustExtract]
P [in TypedExtraction.Elm.ElmExtract]
PT [in TypedExtraction.Rust.RustExtract]
PT [in TypedExtraction.Elm.ElmExtract]
R
RecordSetNotations [in TypedExtraction.Tests.RecordSet]recursor_ex [in TypedExtraction.Tests.ElmExtractTests]
S
SafeHead [in TypedExtraction.Tests.RustExtractTests]T
T [in TypedExtraction.Rust.PluginExtract]T [in TypedExtraction.Rust.RustExtract]
T [in TypedExtraction.Elm.ElmExtract]
TUtil [in TypedExtraction.Rust.RustExtract]
TUtil [in TypedExtraction.Elm.ElmExtract]
type_scheme_ex.LetouzeyExample [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex [in TypedExtraction.Tests.ElmExtractTests]
T2P [in TypedExtraction.Rust.RustExtract]
T2P [in TypedExtraction.Elm.ElmExtract]
Variable Index
F
FixEnv.ind_attrs [in TypedExtraction.Rust.RustExtract]FixEnv.print_term.print_term [in TypedExtraction.Rust.RustExtract]
FixEnv.remaps [in TypedExtraction.Rust.RustExtract]
FixEnv.translate [in TypedExtraction.Elm.ElmExtract]
FixEnv.Σ [in TypedExtraction.Rust.RustExtract]
FixEnv.Σ [in TypedExtraction.Elm.ElmExtract]
Library Index
A
AckB
BernsteinYangTerminationC
CommonE
ElmExtractElmExtractExamples
ElmExtractTests
ElmForms
ExtractExtraction
ExtrRustBasic
ExtrRustCheckedArith
ExtrRustUncheckedArith
I
InternalFixL
LoaderP
PluginExtractPrettyPrinterMonad
Printing
R
RecordSetRecordUpdate
RustExtract
RustExtractTests
S
StringExtraT
TopLevelFixesConstructor Index
A
Add [in TypedExtraction.Tests.ElmForms]E
ex8.MPIConstr [in TypedExtraction.Tests.ElmExtractTests]ex9.MPINAConstr1 [in TypedExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr2 [in TypedExtraction.Tests.ElmExtractTests]
M
MsgName [in TypedExtraction.Tests.ElmForms]MsgPassword [in TypedExtraction.Tests.ElmForms]
MsgPasswordAgain [in TypedExtraction.Tests.ElmForms]
N
none [in TypedExtraction.Tests.ElmForms]S
setter_from_getter [in TypedExtraction.Tests.RecordSet]U
UpdateEntry [in TypedExtraction.Tests.ElmForms]Lemma Index
L
lexicographic_ordering_wf [in TypedExtraction.Tests.Ack]lt_wf_double_ind [in TypedExtraction.Tests.Ack]
lt_wf_ind [in TypedExtraction.Tests.Ack]
R
recursor_ex.test_is_map [in TypedExtraction.Tests.ElmExtractTests]Projection Index
A
any_type_symbol [in TypedExtraction.Rust.RustExtract]any_type_symbol [in TypedExtraction.Elm.ElmExtract]
C
currentEntry [in TypedExtraction.Tests.ElmForms]cur_output_line [in TypedExtraction.Common.PrettyPrinterMonad]
E
elmmd_extract [in TypedExtraction.Tests.ElmForms]errors [in TypedExtraction.Tests.ElmForms]
F
false_elim_def [in TypedExtraction.Elm.ElmExtract]I
indent_stack [in TypedExtraction.Common.PrettyPrinterMonad]N
name [in TypedExtraction.Tests.ElmForms]O
output_lines [in TypedExtraction.Common.PrettyPrinterMonad]P
password [in TypedExtraction.Tests.ElmForms]passwordAgain [in TypedExtraction.Tests.ElmForms]
print_full_names [in TypedExtraction.Rust.RustExtract]
print_full_names [in TypedExtraction.Elm.ElmExtract]
program_preamble [in TypedExtraction.Rust.RustExtract]
R
remap_inline_constant [in TypedExtraction.Rust.Printing]remap_constant [in TypedExtraction.Rust.Printing]
remap_inductive [in TypedExtraction.Rust.Printing]
re_ind_match [in TypedExtraction.Rust.Printing]
re_ind_ctors [in TypedExtraction.Rust.Printing]
re_ind_name [in TypedExtraction.Rust.Printing]
S
seName [in TypedExtraction.Tests.ElmForms]sePassword [in TypedExtraction.Tests.ElmForms]
setter_from_getter [in TypedExtraction.Tests.RecordSet]
T
term_box_symbol [in TypedExtraction.Rust.RustExtract]term_box_symbol [in TypedExtraction.Elm.ElmExtract]
top_preamble [in TypedExtraction.Rust.RustExtract]
type_box_symbol [in TypedExtraction.Rust.RustExtract]
type_box_symbol [in TypedExtraction.Elm.ElmExtract]
U
used_names [in TypedExtraction.Common.PrettyPrinterMonad]users [in TypedExtraction.Tests.ElmForms]
Inductive Index
C
Cmd [in TypedExtraction.Tests.ElmForms]E
ex8.ManyParamsInd [in TypedExtraction.Tests.ElmExtractTests]ex9.ManyParamsIndNonArity [in TypedExtraction.Tests.ElmExtractTests]
M
Msg [in TypedExtraction.Tests.ElmForms]S
SetterFromGetter [in TypedExtraction.Tests.RecordSet]StorageMsg [in TypedExtraction.Tests.ElmForms]
Instance Index
E
ElmBoxes [in TypedExtraction.Tests.ElmForms]ElmBoxes [in TypedExtraction.Tests.ElmExtractExamples]
M
Monad_PrettyPrinter [in TypedExtraction.Common.PrettyPrinterMonad]P
plugin_extract_preamble [in TypedExtraction.Rust.PluginExtract]R
RustConfig [in TypedExtraction.Rust.PluginExtract]RustConfig [in TypedExtraction.Tests.RustExtractTests]
S
StandardBoxes [in TypedExtraction.Tests.ElmExtractTests]Section Index
F
FixEnv [in TypedExtraction.Rust.RustExtract]FixEnv [in TypedExtraction.Elm.ElmExtract]
FixEnv.print_term [in TypedExtraction.Rust.RustExtract]
Definition Index
A
ack [in TypedExtraction.Tests.InternalFix]ack [in TypedExtraction.Tests.Ack]
append [in TypedExtraction.Common.PrettyPrinterMonad]
append_concat [in TypedExtraction.Common.PrettyPrinterMonad]
append_join [in TypedExtraction.Common.PrettyPrinterMonad]
append_nl [in TypedExtraction.Common.PrettyPrinterMonad]
aRelevant [in TypedExtraction.Tests.RecordSet]
C
capitalize [in TypedExtraction.Common.StringExtra]char_to_lower [in TypedExtraction.Common.StringExtra]
char_to_upper [in TypedExtraction.Common.StringExtra]
clean_local_ident [in TypedExtraction.Rust.RustExtract]
clean_global_ident [in TypedExtraction.Rust.RustExtract]
Cmd_sind [in TypedExtraction.Tests.ElmForms]
Cmd_rec [in TypedExtraction.Tests.ElmForms]
Cmd_ind [in TypedExtraction.Tests.ElmForms]
Cmd_rect [in TypedExtraction.Tests.ElmForms]
collect_output [in TypedExtraction.Common.PrettyPrinterMonad]
collect_output_lines [in TypedExtraction.Common.PrettyPrinterMonad]
const_global_ident_of_kername [in TypedExtraction.Rust.RustExtract]
D
default_attrs [in TypedExtraction.Rust.PluginExtract]default_attrs [in TypedExtraction.Tests.RustExtractTests]
divstep [in TypedExtraction.Tests.BernsteinYangTermination]
E
ElmExamples.ackermann [in TypedExtraction.Tests.ElmExtractExamples]ElmExamples.ElmExamples_nth [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_foldl [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_map [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.head_of_repeat_plus_one [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.inc_counter [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.main_and_test [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.Preambule [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.result_foldl [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.result_map [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.result_nth [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_head [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_partial [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_full [in TypedExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred [in TypedExtraction.Tests.ElmExtractExamples]
elm_extraction [in TypedExtraction.Tests.ElmForms]
elm_false_rec [in TypedExtraction.Elm.ElmExtract]
emptyNameError [in TypedExtraction.Tests.ElmForms]
even [in TypedExtraction.Tests.InternalFix]
even_odd [in TypedExtraction.Tests.InternalFix]
extract [in TypedExtraction.Rust.PluginExtract]
extract [in TypedExtraction.Tests.RustExtractTests]
extract [in TypedExtraction.Tests.ElmExtractTests]
extract_def_name_exists [in TypedExtraction.Common.Common]
extract_def_name [in TypedExtraction.Common.Common]
extract_lines [in TypedExtraction.Rust.PluginExtract]
extract_elm_within_rocq [in TypedExtraction.Tests.ElmForms]
extract_rust_within_rocq [in TypedExtraction.Rust.RustExtract]
ex_infix1.test [in TypedExtraction.Tests.ElmExtractTests]
ex_infix1.TT [in TypedExtraction.Tests.ElmExtractTests]
ex1.bar [in TypedExtraction.Tests.RustExtractTests]
ex1.bar [in TypedExtraction.Tests.ElmExtractTests]
ex1.ex1_test [in TypedExtraction.Tests.RustExtractTests]
ex1.ex1_test [in TypedExtraction.Tests.ElmExtractTests]
ex1.foo [in TypedExtraction.Tests.RustExtractTests]
ex1.foo [in TypedExtraction.Tests.ElmExtractTests]
ex10.ex10_test [in TypedExtraction.Tests.ElmExtractTests]
ex10.foo [in TypedExtraction.Tests.ElmExtractTests]
ex11.Monad_test [in TypedExtraction.Tests.ElmExtractTests]
ex12.idT [in TypedExtraction.Tests.ElmExtractTests]
ex12.test [in TypedExtraction.Tests.ElmExtractTests]
ex12.weird_id [in TypedExtraction.Tests.ElmExtractTests]
ex13.opt [in TypedExtraction.Tests.ElmExtractTests]
ex13.test [in TypedExtraction.Tests.ElmExtractTests]
ex13.unwrap [in TypedExtraction.Tests.ElmExtractTests]
ex2.bar [in TypedExtraction.Tests.RustExtractTests]
ex2.bar [in TypedExtraction.Tests.ElmExtractTests]
ex2.ex2_test [in TypedExtraction.Tests.RustExtractTests]
ex2.ex2_test [in TypedExtraction.Tests.ElmExtractTests]
ex2.foo [in TypedExtraction.Tests.RustExtractTests]
ex2.foo [in TypedExtraction.Tests.ElmExtractTests]
ex2.only_in_type [in TypedExtraction.Tests.RustExtractTests]
ex2.only_in_type [in TypedExtraction.Tests.ElmExtractTests]
ex3.bar [in TypedExtraction.Tests.ElmExtractTests]
ex3.baz [in TypedExtraction.Tests.ElmExtractTests]
ex3.ex3_test [in TypedExtraction.Tests.ElmExtractTests]
ex3.foo [in TypedExtraction.Tests.ElmExtractTests]
ex3.test [in TypedExtraction.Tests.RustExtractTests]
ex4.ack [in TypedExtraction.Tests.RustExtractTests]
ex4.ex4_test [in TypedExtraction.Tests.ElmExtractTests]
ex4.foo [in TypedExtraction.Tests.ElmExtractTests]
ex4.test [in TypedExtraction.Tests.RustExtractTests]
ex5.code [in TypedExtraction.Tests.RustExtractTests]
ex5.ex5_test [in TypedExtraction.Tests.ElmExtractTests]
ex5.foo [in TypedExtraction.Tests.ElmExtractTests]
ex5.test [in TypedExtraction.Tests.RustExtractTests]
ex6.bar [in TypedExtraction.Tests.ElmExtractTests]
ex6.baz [in TypedExtraction.Tests.ElmExtractTests]
ex6.ex6_test [in TypedExtraction.Tests.ElmExtractTests]
ex6.foo [in TypedExtraction.Tests.ElmExtractTests]
ex7.bar [in TypedExtraction.Tests.ElmExtractTests]
ex7.ex7_test [in TypedExtraction.Tests.ElmExtractTests]
ex7.foo [in TypedExtraction.Tests.ElmExtractTests]
ex8.ex8_test [in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_sind [in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rec [in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_ind [in TypedExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rect [in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_test [in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_sind [in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rec [in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_ind [in TypedExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rect [in TypedExtraction.Tests.ElmExtractTests]
F
finish_print [in TypedExtraction.Common.PrettyPrinterMonad]finish_print_lines [in TypedExtraction.Common.PrettyPrinterMonad]
fresh [in TypedExtraction.Rust.RustExtract]
fresh [in TypedExtraction.Elm.ElmExtract]
fresh_name [in TypedExtraction.Common.PrettyPrinterMonad]
fresh_ty_arg_name [in TypedExtraction.Rust.RustExtract]
fresh_ident [in TypedExtraction.Rust.RustExtract]
fresh_ty_arg_name [in TypedExtraction.Elm.ElmExtract]
fresh_ident [in TypedExtraction.Elm.ElmExtract]
G
general_wrapped [in TypedExtraction.Tests.ElmForms]general_extract [in TypedExtraction.Tests.ElmExtractTests]
general_wrapped [in TypedExtraction.Tests.ElmExtractExamples]
get_current_line_length [in TypedExtraction.Common.PrettyPrinterMonad]
get_used_names [in TypedExtraction.Common.PrettyPrinterMonad]
get_indent [in TypedExtraction.Common.PrettyPrinterMonad]
get_num_inline_args [in TypedExtraction.Rust.RustExtract]
get_ind_ident [in TypedExtraction.Rust.RustExtract]
get_ty_const_ident [in TypedExtraction.Rust.RustExtract]
get_infix [in TypedExtraction.Elm.ElmExtract]
get_ty_arg_name [in TypedExtraction.Elm.ElmExtract]
get_ident_name [in TypedExtraction.Elm.ElmExtract]
get_ctor_name [in TypedExtraction.Elm.ElmExtract]
get_ty_name [in TypedExtraction.Elm.ElmExtract]
get_fun_name [in TypedExtraction.Elm.ElmExtract]
H
header_and_imports [in TypedExtraction.Tests.ElmForms]hex_of_Z [in TypedExtraction.Common.StringExtra]
hex_of_nat [in TypedExtraction.Common.StringExtra]
hex_of_N [in TypedExtraction.Common.StringExtra]
hex_of_positive [in TypedExtraction.Common.StringExtra]
I
indent_size [in TypedExtraction.Rust.RustExtract]indent_size [in TypedExtraction.Elm.ElmExtract]
ind_attr_map [in TypedExtraction.Rust.RustExtract]
initModel [in TypedExtraction.Tests.ElmForms]
is_letter [in TypedExtraction.Common.StringExtra]
is_polymorphic [in TypedExtraction.Rust.RustExtract]
L
last_index_of [in TypedExtraction.Common.StringExtra]lexicographic_ordering [in TypedExtraction.Tests.Ack]
lines [in TypedExtraction.Common.StringExtra]
lookup_ind_decl [in TypedExtraction.Rust.RustExtract]
lookup_mind [in TypedExtraction.Rust.RustExtract]
lookup_ind_decl [in TypedExtraction.Elm.ElmExtract]
lookup_mind [in TypedExtraction.Elm.ElmExtract]
M
make_setters [in TypedExtraction.Tests.RecordSet]map_cur_output_line [in TypedExtraction.Common.PrettyPrinterMonad]
map_used_names [in TypedExtraction.Common.PrettyPrinterMonad]
map_indent_stack [in TypedExtraction.Common.PrettyPrinterMonad]
map_pps [in TypedExtraction.Common.PrettyPrinterMonad]
min_needs_n_steps_nat [in TypedExtraction.Tests.BernsteinYangTermination]
monad_append_concat [in TypedExtraction.Common.PrettyPrinterMonad]
monad_append_join [in TypedExtraction.Common.PrettyPrinterMonad]
Msg_sind [in TypedExtraction.Tests.ElmForms]
Msg_rec [in TypedExtraction.Tests.ElmForms]
Msg_ind [in TypedExtraction.Tests.ElmForms]
Msg_rect [in TypedExtraction.Tests.ElmForms]
N
nat_syn_to_nat [in TypedExtraction.Common.Common]nat_shiftl [in TypedExtraction.Tests.BernsteinYangTermination]
needs_block [in TypedExtraction.Rust.RustExtract]
needs_n_steps [in TypedExtraction.Tests.BernsteinYangTermination]
nl [in TypedExtraction.Common.Common]
Nlog2up_nat [in TypedExtraction.Common.StringExtra]
nonEmptyString [in TypedExtraction.Tests.ElmForms]
no_remaps [in TypedExtraction.Rust.Printing]
no_check_args [in TypedExtraction.Tests.ElmExtractTests]
no_check_args [in TypedExtraction.Tests.ElmExtractExamples]
N_syn_to_nat [in TypedExtraction.Common.Common]
O
odd [in TypedExtraction.Tests.InternalFix]odd [in TypedExtraction.Tests.BernsteinYangTermination]
optimize [in TypedExtraction.Rust.TopLevelFixes]
optimize_env [in TypedExtraction.Rust.TopLevelFixes]
optimize_decl [in TypedExtraction.Rust.TopLevelFixes]
optimize_aux [in TypedExtraction.Rust.TopLevelFixes]
P
parens [in TypedExtraction.Common.Common]parenthesize_ty_app_arg [in TypedExtraction.Rust.RustExtract]
parenthesize_case_discriminee [in TypedExtraction.Rust.RustExtract]
parenthesize_app_arg [in TypedExtraction.Rust.RustExtract]
parenthesize_app_head [in TypedExtraction.Rust.RustExtract]
parenthesize_ind_ctor_ty [in TypedExtraction.Elm.ElmExtract]
parenthesize_ty_app_arg [in TypedExtraction.Elm.ElmExtract]
parenthesize_prod_domain [in TypedExtraction.Elm.ElmExtract]
parenthesize_case_branch [in TypedExtraction.Elm.ElmExtract]
parenthesize_case_discriminee [in TypedExtraction.Elm.ElmExtract]
parenthesize_app_arg [in TypedExtraction.Elm.ElmExtract]
parenthesize_app_head [in TypedExtraction.Elm.ElmExtract]
passwordIsTooShortError [in TypedExtraction.Tests.ElmForms]
passwordsDoNotMatchError [in TypedExtraction.Tests.ElmForms]
pop_use [in TypedExtraction.Common.PrettyPrinterMonad]
pop_indent [in TypedExtraction.Common.PrettyPrinterMonad]
pos_syn_to_nat [in TypedExtraction.Common.Common]
pos_syn_to_nat_aux [in TypedExtraction.Common.Common]
preamble [in TypedExtraction.Tests.ElmForms]
prefix_spaces [in TypedExtraction.Common.PrettyPrinterMonad]
PrettyPrinter [in TypedExtraction.Common.PrettyPrinterMonad]
printer_fail [in TypedExtraction.Common.PrettyPrinterMonad]
print_list [in TypedExtraction.Common.Common]
print_program [in TypedExtraction.Rust.RustExtract]
print_decls [in TypedExtraction.Rust.RustExtract]
print_decls_aux [in TypedExtraction.Rust.RustExtract]
print_type_alias [in TypedExtraction.Rust.RustExtract]
print_mutual_inductive_body [in TypedExtraction.Rust.RustExtract]
print_ind_ctor_definition [in TypedExtraction.Rust.RustExtract]
print_constant [in TypedExtraction.Rust.RustExtract]
print_term [in TypedExtraction.Rust.RustExtract]
print_remapped_case [in TypedExtraction.Rust.RustExtract]
print_case [in TypedExtraction.Rust.RustExtract]
print_const [in TypedExtraction.Rust.RustExtract]
print_constructor [in TypedExtraction.Rust.RustExtract]
print_app [in TypedExtraction.Rust.RustExtract]
print_type [in TypedExtraction.Rust.RustExtract]
print_type_aux [in TypedExtraction.Rust.RustExtract]
print_parenthesized_with [in TypedExtraction.Rust.RustExtract]
print_parenthesized [in TypedExtraction.Rust.RustExtract]
print_ind [in TypedExtraction.Rust.RustExtract]
print_env [in TypedExtraction.Elm.ElmExtract]
print_type_alias [in TypedExtraction.Elm.ElmExtract]
print_mutual_inductive_body [in TypedExtraction.Elm.ElmExtract]
print_ind_ctor_definition [in TypedExtraction.Elm.ElmExtract]
print_constant [in TypedExtraction.Elm.ElmExtract]
print_term [in TypedExtraction.Elm.ElmExtract]
print_infix_match_branch [in TypedExtraction.Elm.ElmExtract]
print_define_term [in TypedExtraction.Elm.ElmExtract]
print_type [in TypedExtraction.Elm.ElmExtract]
print_parenthesized [in TypedExtraction.Elm.ElmExtract]
print_ind_ctor [in TypedExtraction.Elm.ElmExtract]
print_ind [in TypedExtraction.Elm.ElmExtract]
push_use [in TypedExtraction.Common.PrettyPrinterMonad]
push_indent [in TypedExtraction.Common.PrettyPrinterMonad]
Q
quote_recursively_body [in TypedExtraction.Common.Common]R
recursor_ex.ex_test [in TypedExtraction.Tests.ElmExtractTests]recursor_ex.test [in TypedExtraction.Tests.ElmExtractTests]
remap [in TypedExtraction.Common.Common]
remove_char [in TypedExtraction.Common.StringExtra]
replace [in TypedExtraction.Common.StringExtra]
replace_char [in TypedExtraction.Common.StringExtra]
result_of_option [in TypedExtraction.Common.Common]
result_of_typing_result [in TypedExtraction.Common.Common]
result_string_err [in TypedExtraction.Common.PrettyPrinterMonad]
result_bytestring_err [in TypedExtraction.Tests.ElmExtractTests]
result_err_bytestring [in TypedExtraction.Tests.ElmExtractExamples]
S
SafeHead.head_of_repeat_plus_one [in TypedExtraction.Tests.RustExtractTests]SafeHead.safe_head [in TypedExtraction.Tests.RustExtractTests]
SafeHead.test [in TypedExtraction.Tests.RustExtractTests]
seNames [in TypedExtraction.Tests.ElmForms]
shiftl [in TypedExtraction.Tests.BernsteinYangTermination]
shiftr [in TypedExtraction.Tests.BernsteinYangTermination]
starts_with [in TypedExtraction.Common.StringExtra]
starts_with_cont [in TypedExtraction.Common.StringExtra]
steps [in TypedExtraction.Tests.BernsteinYangTermination]
StorageMsg_sind [in TypedExtraction.Tests.ElmForms]
StorageMsg_rec [in TypedExtraction.Tests.ElmForms]
StorageMsg_ind [in TypedExtraction.Tests.ElmForms]
StorageMsg_rect [in TypedExtraction.Tests.ElmForms]
string_of_list [in TypedExtraction.Common.Common]
string_of_list_aux [in TypedExtraction.Common.Common]
string_of_env_error [in TypedExtraction.Common.Common]
string_of_env_error [in TypedExtraction.Common.PrettyPrinterMonad]
string_of_Z [in TypedExtraction.Common.StringExtra]
string_of_positive [in TypedExtraction.Common.StringExtra]
string_of_nat [in TypedExtraction.Common.StringExtra]
string_of_N [in TypedExtraction.Common.StringExtra]
str_split [in TypedExtraction.Common.StringExtra]
str_map [in TypedExtraction.Common.StringExtra]
str_rev [in TypedExtraction.Common.StringExtra]
substring_count [in TypedExtraction.Common.StringExtra]
substring_from [in TypedExtraction.Common.StringExtra]
T
toValidStoredEntry [in TypedExtraction.Tests.ElmForms]to_string_name [in TypedExtraction.Common.Common]
to_globref [in TypedExtraction.Common.Common]
to_kername [in TypedExtraction.Common.Common]
to_inline [in TypedExtraction.Tests.ElmForms]
to_lower [in TypedExtraction.Common.StringExtra]
to_upper [in TypedExtraction.Common.StringExtra]
transform [in TypedExtraction.Rust.TopLevelFixes]
TT [in TypedExtraction.Tests.ElmForms]
type_scheme_ex.singleton_vec_test [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.singleton_vec [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.vec [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied_test [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_test [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3 [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.P [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple_test [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow_test [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow [in TypedExtraction.Tests.ElmExtractTests]
type_scheme_ex.general_extract_tc [in TypedExtraction.Tests.ElmExtractTests]
ty_const_global_ident_of_kername [in TypedExtraction.Rust.RustExtract]
U
uncapitalize [in TypedExtraction.Common.StringExtra]updateEntry [in TypedExtraction.Tests.ElmForms]
updateModel [in TypedExtraction.Tests.ElmForms]
userAlreadyExistsError [in TypedExtraction.Tests.ElmForms]
USER_FORM_APP [in TypedExtraction.Tests.ElmForms]
V
validateModel [in TypedExtraction.Tests.ElmForms]ValidEntry [in TypedExtraction.Tests.ElmForms]
validPassword [in TypedExtraction.Tests.ElmForms]
ValidStoredEntry [in TypedExtraction.Tests.ElmForms]
W
W [in TypedExtraction.Tests.BernsteinYangTermination]wrapped [in TypedExtraction.Tests.ElmExtractExamples]
wrap_result [in TypedExtraction.Common.PrettyPrinterMonad]
wrap_option [in TypedExtraction.Common.PrettyPrinterMonad]
wrap_typing_result [in TypedExtraction.Common.PrettyPrinterMonad]
wrap_EnvCheck [in TypedExtraction.Common.PrettyPrinterMonad]
Z
Z_syn_to_Z [in TypedExtraction.Common.Common]_
_Zneg [in TypedExtraction.Common.Common]_Zpos [in TypedExtraction.Common.Common]
_Z0 [in TypedExtraction.Common.Common]
_Npos [in TypedExtraction.Common.Common]
_N0 [in TypedExtraction.Common.Common]
_xH [in TypedExtraction.Common.Common]
_xO [in TypedExtraction.Common.Common]
_xI [in TypedExtraction.Common.Common]
Record Index
E
ElmMod [in TypedExtraction.Tests.ElmForms]ElmPrintConfig [in TypedExtraction.Elm.ElmExtract]
Entry [in TypedExtraction.Tests.ElmForms]
M
Model [in TypedExtraction.Tests.ElmForms]P
Preamble [in TypedExtraction.Rust.RustExtract]PrettyPrinterState [in TypedExtraction.Common.PrettyPrinterMonad]
R
remapped_inductive [in TypedExtraction.Rust.Printing]remaps [in TypedExtraction.Rust.Printing]
RustPrintConfig [in TypedExtraction.Rust.RustExtract]
S
SetterFromGetter [in TypedExtraction.Tests.RecordSet]StoredEntry [in TypedExtraction.Tests.ElmForms]
| 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 | (471 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 | (12 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 | (43 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 | (6 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 | (22 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 | (10 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 | (4 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 | (31 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 | (6 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 | (7 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 | (3 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 | (316 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 | (11 entries) |