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 (311 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 (28 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 (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)
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)
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)
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 (19 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 (1 entry)
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 (206 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 (7 entries)

Global Index

A

ack [definition, in ElmExtraction.Tests.Ack]
Ack [library]
Add [constructor, in ElmExtraction.Tests.ElmForms]
any_type_symbol [projection, in ElmExtraction.ElmExtract]
append [definition, in ElmExtraction.PrettyPrinterMonad]
append_concat [definition, in ElmExtraction.PrettyPrinterMonad]
append_join [definition, in ElmExtraction.PrettyPrinterMonad]
append_nl [definition, in ElmExtraction.PrettyPrinterMonad]
aRelevant [definition, in ElmExtraction.Tests.RecordSet]


B

bs_to_s [abbreviation, in ElmExtraction.ElmExtract]
bs_to_s [abbreviation, in ElmExtraction.PrettyPrinterMonad]


C

capitalize [definition, in ElmExtraction.StringExtra]
char_to_lower [definition, in ElmExtraction.StringExtra]
char_to_upper [definition, in ElmExtraction.StringExtra]
Cmd [inductive, in ElmExtraction.Tests.ElmForms]
Cmd_sind [definition, in ElmExtraction.Tests.ElmForms]
Cmd_rec [definition, in ElmExtraction.Tests.ElmForms]
Cmd_ind [definition, in ElmExtraction.Tests.ElmForms]
Cmd_rect [definition, in ElmExtraction.Tests.ElmForms]
collect_output [definition, in ElmExtraction.PrettyPrinterMonad]
collect_output_lines [definition, in ElmExtraction.PrettyPrinterMonad]
Common [library]
currentEntry [projection, in ElmExtraction.Tests.ElmForms]
cur_output_line [projection, in ElmExtraction.PrettyPrinterMonad]


E

E [module, in ElmExtraction.ElmExtract]
EF [module, in ElmExtraction.ElmExtract]
ElmBoxes [instance, in ElmExtraction.Tests.ElmExtractExamples]
ElmBoxes [instance, in ElmExtraction.Tests.ElmForms]
ElmExamples [module, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ackermann [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmExamples_nth [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_foldl [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_map [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.head_of_repeat_plus_one [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.inc_counter [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.main_and_test [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.Preambule [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.result_foldl [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.result_map [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.result_nth [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_head [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_partial [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_full [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred [definition, in ElmExtraction.Tests.ElmExtractExamples]
ElmExtract [library]
ElmExtractExamples [library]
ElmExtractTests [library]
ElmForms [library]
elmmd_extract [projection, in ElmExtraction.Tests.ElmForms]
ElmMod [record, in ElmExtraction.Tests.ElmForms]
ElmPrintConfig [record, in ElmExtraction.ElmExtract]
elm_false_rec [definition, in ElmExtraction.ElmExtract]
elm_extraction [definition, in ElmExtraction.Tests.ElmForms]
emptyNameError [definition, in ElmExtraction.Tests.ElmForms]
Entry [record, in ElmExtraction.Tests.ElmForms]
errors [projection, in ElmExtraction.Tests.ElmForms]
Ex [module, in ElmExtraction.ElmExtract]
extract [definition, in ElmExtraction.Tests.ElmExtractTests]
extract_def_name_exists [definition, in ElmExtraction.Common]
extract_def_name [definition, in ElmExtraction.Common]
extract_elm_within_coq [definition, in ElmExtraction.Tests.ElmForms]
ex_infix1.test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex_infix1.TT [definition, in ElmExtraction.Tests.ElmExtractTests]
ex_infix1 [module, in ElmExtraction.Tests.ElmExtractTests]
ex1 [module, in ElmExtraction.Tests.ElmExtractTests]
ex1.bar [definition, in ElmExtraction.Tests.ElmExtractTests]
ex1.ex1_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex1.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex10 [module, in ElmExtraction.Tests.ElmExtractTests]
ex10.ex10_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex10.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex11 [module, in ElmExtraction.Tests.ElmExtractTests]
ex11.Monad_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex12 [module, in ElmExtraction.Tests.ElmExtractTests]
ex12.idT [definition, in ElmExtraction.Tests.ElmExtractTests]
ex12.test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex12.weird_id [definition, in ElmExtraction.Tests.ElmExtractTests]
ex13 [module, in ElmExtraction.Tests.ElmExtractTests]
ex13.opt [definition, in ElmExtraction.Tests.ElmExtractTests]
ex13.test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex13.unwrap [definition, in ElmExtraction.Tests.ElmExtractTests]
ex2 [module, in ElmExtraction.Tests.ElmExtractTests]
ex2.bar [definition, in ElmExtraction.Tests.ElmExtractTests]
ex2.ex2_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex2.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex2.only_in_type [definition, in ElmExtraction.Tests.ElmExtractTests]
ex3 [module, in ElmExtraction.Tests.ElmExtractTests]
ex3.bar [definition, in ElmExtraction.Tests.ElmExtractTests]
ex3.baz [definition, in ElmExtraction.Tests.ElmExtractTests]
ex3.ex3_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex3.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex4 [module, in ElmExtraction.Tests.ElmExtractTests]
ex4.ex4_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex4.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex5 [module, in ElmExtraction.Tests.ElmExtractTests]
ex5.ex5_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex5.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex6 [module, in ElmExtraction.Tests.ElmExtractTests]
ex6.bar [definition, in ElmExtraction.Tests.ElmExtractTests]
ex6.baz [definition, in ElmExtraction.Tests.ElmExtractTests]
ex6.ex6_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex6.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex7 [module, in ElmExtraction.Tests.ElmExtractTests]
ex7.bar [definition, in ElmExtraction.Tests.ElmExtractTests]
ex7.ex7_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex7.foo [definition, in ElmExtraction.Tests.ElmExtractTests]
ex8 [module, in ElmExtraction.Tests.ElmExtractTests]
ex8.ex8_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd [inductive, in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_sind [definition, in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rec [definition, in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_ind [definition, in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rect [definition, in ElmExtraction.Tests.ElmExtractTests]
ex8.MPIConstr [constructor, in ElmExtraction.Tests.ElmExtractTests]
ex9 [module, in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity [inductive, in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_test [definition, in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_sind [definition, in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rec [definition, in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_ind [definition, in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rect [definition, in ElmExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr1 [constructor, in ElmExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr2 [constructor, in ElmExtraction.Tests.ElmExtractTests]


F

false_elim_def [projection, in ElmExtraction.ElmExtract]
finish_print [definition, in ElmExtraction.PrettyPrinterMonad]
finish_print_lines [definition, in ElmExtraction.PrettyPrinterMonad]
FixEnv [section, in ElmExtraction.ElmExtract]
_ ^ _ [notation, in ElmExtraction.ElmExtract]
fresh [definition, in ElmExtraction.ElmExtract]
fresh_ty_arg_name [definition, in ElmExtraction.ElmExtract]
fresh_ident [definition, in ElmExtraction.ElmExtract]
fresh_name [definition, in ElmExtraction.PrettyPrinterMonad]


G

general_extract [definition, in ElmExtraction.Tests.ElmExtractTests]
general_wrapped [definition, in ElmExtraction.Tests.ElmExtractExamples]
general_wrapped [definition, in ElmExtraction.Tests.ElmForms]
get_infix [definition, in ElmExtraction.ElmExtract]
get_ty_arg_name [definition, in ElmExtraction.ElmExtract]
get_ident_name [definition, in ElmExtraction.ElmExtract]
get_ctor_name [definition, in ElmExtraction.ElmExtract]
get_ty_name [definition, in ElmExtraction.ElmExtract]
get_fun_name [definition, in ElmExtraction.ElmExtract]
get_current_line_length [definition, in ElmExtraction.PrettyPrinterMonad]
get_used_names [definition, in ElmExtraction.PrettyPrinterMonad]
get_indent [definition, in ElmExtraction.PrettyPrinterMonad]


H

header_and_imports [definition, in ElmExtraction.Tests.ElmForms]


I

indent_size [definition, in ElmExtraction.ElmExtract]
indent_stack [projection, in ElmExtraction.PrettyPrinterMonad]
initModel [definition, in ElmExtraction.Tests.ElmForms]
is_letter [definition, in ElmExtraction.StringExtra]


L

lexicographic_ordering_wf [lemma, in ElmExtraction.Tests.Ack]
lexicographic_ordering [definition, in ElmExtraction.Tests.Ack]
lines [definition, in ElmExtraction.StringExtra]
lookup_ind_decl [definition, in ElmExtraction.ElmExtract]
lookup_mind [definition, in ElmExtraction.ElmExtract]
lt_wf_double_ind [lemma, in ElmExtraction.Tests.Ack]
lt_wf_ind [lemma, in ElmExtraction.Tests.Ack]


M

make_setters [definition, in ElmExtraction.Tests.RecordSet]
map_cur_output_line [definition, in ElmExtraction.PrettyPrinterMonad]
map_used_names [definition, in ElmExtraction.PrettyPrinterMonad]
map_indent_stack [definition, in ElmExtraction.PrettyPrinterMonad]
map_pps [definition, in ElmExtraction.PrettyPrinterMonad]
Model [record, in ElmExtraction.Tests.ElmForms]
monad_append_concat [definition, in ElmExtraction.PrettyPrinterMonad]
monad_append_join [definition, in ElmExtraction.PrettyPrinterMonad]
Monad_PrettyPrinter [instance, in ElmExtraction.PrettyPrinterMonad]
Msg [inductive, in ElmExtraction.Tests.ElmForms]
MsgName [constructor, in ElmExtraction.Tests.ElmForms]
MsgPassword [constructor, in ElmExtraction.Tests.ElmForms]
MsgPasswordAgain [constructor, in ElmExtraction.Tests.ElmForms]
Msg_sind [definition, in ElmExtraction.Tests.ElmForms]
Msg_rec [definition, in ElmExtraction.Tests.ElmForms]
Msg_ind [definition, in ElmExtraction.Tests.ElmForms]
Msg_rect [definition, in ElmExtraction.Tests.ElmForms]


N

name [projection, in ElmExtraction.Tests.ElmForms]
nl [definition, in ElmExtraction.Common]
Nlog2up_nat [definition, in ElmExtraction.StringExtra]
none [constructor, in ElmExtraction.Tests.ElmForms]
nonEmptyString [definition, in ElmExtraction.Tests.ElmForms]
no_check_args [definition, in ElmExtraction.Tests.ElmExtractTests]
no_check_args [definition, in ElmExtraction.Tests.ElmExtractExamples]


O

output_lines [projection, in ElmExtraction.PrettyPrinterMonad]


P

P [module, in ElmExtraction.ElmExtract]
P [module, in ElmExtraction.PrettyPrinterMonad]
parens [definition, in ElmExtraction.Common]
parenthesize_ind_ctor_ty [definition, in ElmExtraction.ElmExtract]
parenthesize_ty_app_arg [definition, in ElmExtraction.ElmExtract]
parenthesize_prod_domain [definition, in ElmExtraction.ElmExtract]
parenthesize_case_branch [definition, in ElmExtraction.ElmExtract]
parenthesize_case_discriminee [definition, in ElmExtraction.ElmExtract]
parenthesize_app_arg [definition, in ElmExtraction.ElmExtract]
parenthesize_app_head [definition, in ElmExtraction.ElmExtract]
password [projection, in ElmExtraction.Tests.ElmForms]
passwordAgain [projection, in ElmExtraction.Tests.ElmForms]
passwordIsTooShortError [definition, in ElmExtraction.Tests.ElmForms]
passwordsDoNotMatchError [definition, in ElmExtraction.Tests.ElmForms]
pop_use [definition, in ElmExtraction.PrettyPrinterMonad]
pop_indent [definition, in ElmExtraction.PrettyPrinterMonad]
preamble [definition, in ElmExtraction.Tests.ElmForms]
prefix_spaces [definition, in ElmExtraction.PrettyPrinterMonad]
PrettyPrinter [definition, in ElmExtraction.PrettyPrinterMonad]
PrettyPrinterMonad [library]
PrettyPrinterState [record, in ElmExtraction.PrettyPrinterMonad]
printer_fail [definition, in ElmExtraction.PrettyPrinterMonad]
print_env [definition, in ElmExtraction.ElmExtract]
print_type_alias [definition, in ElmExtraction.ElmExtract]
print_mutual_inductive_body [definition, in ElmExtraction.ElmExtract]
print_ind_ctor_definition [definition, in ElmExtraction.ElmExtract]
print_constant [definition, in ElmExtraction.ElmExtract]
print_term [definition, in ElmExtraction.ElmExtract]
print_infix_match_branch [definition, in ElmExtraction.ElmExtract]
print_define_term [definition, in ElmExtraction.ElmExtract]
print_type [definition, in ElmExtraction.ElmExtract]
print_parenthesized [definition, in ElmExtraction.ElmExtract]
print_ind_ctor [definition, in ElmExtraction.ElmExtract]
print_ind [definition, in ElmExtraction.ElmExtract]
print_full_names [projection, in ElmExtraction.ElmExtract]
PT [module, in ElmExtraction.ElmExtract]
push_use [definition, in ElmExtraction.PrettyPrinterMonad]
push_indent [definition, in ElmExtraction.PrettyPrinterMonad]


R

RecordSet [library]
RecordSetNotations [module, in ElmExtraction.Tests.RecordSet]
_ <| _ := _ |> (record_set) [notation, in ElmExtraction.Tests.RecordSet]
_ <| _ ::= _ |> (record_set) [notation, in ElmExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ := _ |> [notation, in ElmExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ ::= _ |> [notation, in ElmExtraction.Tests.RecordSet]
RecordUpdate [library]
recursor_ex.ex_test [definition, in ElmExtraction.Tests.ElmExtractTests]
recursor_ex.test_is_map [lemma, in ElmExtraction.Tests.ElmExtractTests]
recursor_ex.test [definition, in ElmExtraction.Tests.ElmExtractTests]
recursor_ex [module, in ElmExtraction.Tests.ElmExtractTests]
remap [definition, in ElmExtraction.Common]
remove_char [definition, in ElmExtraction.StringExtra]
replace_char [definition, in ElmExtraction.StringExtra]
result_of_option [definition, in ElmExtraction.Common]
result_of_typing_result [definition, in ElmExtraction.Common]
result_bytestring_err [definition, in ElmExtraction.Tests.ElmExtractTests]
result_string_err [definition, in ElmExtraction.PrettyPrinterMonad]
result_err_bytestring [definition, in ElmExtraction.Tests.ElmExtractExamples]


S

seName [projection, in ElmExtraction.Tests.ElmForms]
seNames [definition, in ElmExtraction.Tests.ElmForms]
sePassword [projection, in ElmExtraction.Tests.ElmForms]
SetterFromGetter [record, in ElmExtraction.Tests.RecordSet]
SetterFromGetter [inductive, in ElmExtraction.Tests.RecordSet]
setter_from_getter [projection, in ElmExtraction.Tests.RecordSet]
setter_from_getter [constructor, in ElmExtraction.Tests.RecordSet]
StandardBoxes [instance, in ElmExtraction.Tests.ElmExtractTests]
StorageMsg [inductive, in ElmExtraction.Tests.ElmForms]
StorageMsg_sind [definition, in ElmExtraction.Tests.ElmForms]
StorageMsg_rec [definition, in ElmExtraction.Tests.ElmForms]
StorageMsg_ind [definition, in ElmExtraction.Tests.ElmForms]
StorageMsg_rect [definition, in ElmExtraction.Tests.ElmForms]
StoredEntry [record, in ElmExtraction.Tests.ElmForms]
StringExtra [library]
string_of_env_error [definition, in ElmExtraction.Common]
string_of_env_error [definition, in ElmExtraction.PrettyPrinterMonad]
string_of_nat [definition, in ElmExtraction.StringExtra]
string_of_N [definition, in ElmExtraction.StringExtra]
substring_count [definition, in ElmExtraction.StringExtra]
substring_from [definition, in ElmExtraction.StringExtra]
s_to_bs [abbreviation, in ElmExtraction.ElmExtract]
s_to_bs [abbreviation, in ElmExtraction.PrettyPrinterMonad]


T

T [module, in ElmExtraction.ElmExtract]
term_box_symbol [projection, in ElmExtraction.ElmExtract]
toValidStoredEntry [definition, in ElmExtraction.Tests.ElmForms]
to_string_name [definition, in ElmExtraction.Common]
to_globref [definition, in ElmExtraction.Common]
to_kername [definition, in ElmExtraction.Common]
to_inline [definition, in ElmExtraction.Tests.ElmForms]
TT [definition, in ElmExtraction.Tests.ElmForms]
TUtil [module, in ElmExtraction.ElmExtract]
type_scheme_ex.singleton_vec_test [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.singleton_vec [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.vec [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied_test [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_test [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3 [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.P [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample [module, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple_test [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow_test [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.general_extract_tc [definition, in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex [module, in ElmExtraction.Tests.ElmExtractTests]
type_box_symbol [projection, in ElmExtraction.ElmExtract]
T2P [module, in ElmExtraction.ElmExtract]


U

uncapitalize [definition, in ElmExtraction.StringExtra]
UpdateEntry [constructor, in ElmExtraction.Tests.ElmForms]
updateEntry [definition, in ElmExtraction.Tests.ElmForms]
updateModel [definition, in ElmExtraction.Tests.ElmForms]
used_names [projection, in ElmExtraction.PrettyPrinterMonad]
userAlreadyExistsError [definition, in ElmExtraction.Tests.ElmForms]
users [projection, in ElmExtraction.Tests.ElmForms]
USER_FORM_APP [definition, in ElmExtraction.Tests.ElmForms]


V

validateModel [definition, in ElmExtraction.Tests.ElmForms]
ValidEntry [definition, in ElmExtraction.Tests.ElmForms]
validPassword [definition, in ElmExtraction.Tests.ElmForms]
ValidStoredEntry [definition, in ElmExtraction.Tests.ElmForms]


W

wrapped [definition, in ElmExtraction.Tests.ElmExtractExamples]
wrap_result [definition, in ElmExtraction.PrettyPrinterMonad]
wrap_option [definition, in ElmExtraction.PrettyPrinterMonad]
wrap_typing_result [definition, in ElmExtraction.PrettyPrinterMonad]
wrap_EnvCheck [definition, in ElmExtraction.PrettyPrinterMonad]


other

<$ _ ; _ ; .. ; _ $> (string_scope) [notation, in ElmExtraction.StringExtra]
bs_to_s _ [notation, in ElmExtraction.Tests.ElmExtractTests]
remap_ctor _ of _ to _ [notation, in ElmExtraction.Tests.ElmForms]
string_literal _ [notation, in ElmExtraction.Tests.ElmForms]
s_to_bs _ [notation, in ElmExtraction.Tests.ElmExtractTests]
<! _ !> [notation, in ElmExtraction.Common]
<%% _ %%> [notation, in ElmExtraction.Common]



Notation Index

F

_ ^ _ [in ElmExtraction.ElmExtract]


R

_ <| _ := _ |> (record_set) [in ElmExtraction.Tests.RecordSet]
_ <| _ ::= _ |> (record_set) [in ElmExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ := _ |> [in ElmExtraction.Tests.RecordSet]
_ <| _ ; _ ; .. ; _ ::= _ |> [in ElmExtraction.Tests.RecordSet]


other

<$ _ ; _ ; .. ; _ $> (string_scope) [in ElmExtraction.StringExtra]
bs_to_s _ [in ElmExtraction.Tests.ElmExtractTests]
remap_ctor _ of _ to _ [in ElmExtraction.Tests.ElmForms]
string_literal _ [in ElmExtraction.Tests.ElmForms]
s_to_bs _ [in ElmExtraction.Tests.ElmExtractTests]
<! _ !> [in ElmExtraction.Common]
<%% _ %%> [in ElmExtraction.Common]



Module Index

E

E [in ElmExtraction.ElmExtract]
EF [in ElmExtraction.ElmExtract]
ElmExamples [in ElmExtraction.Tests.ElmExtractExamples]
Ex [in ElmExtraction.ElmExtract]
ex_infix1 [in ElmExtraction.Tests.ElmExtractTests]
ex1 [in ElmExtraction.Tests.ElmExtractTests]
ex10 [in ElmExtraction.Tests.ElmExtractTests]
ex11 [in ElmExtraction.Tests.ElmExtractTests]
ex12 [in ElmExtraction.Tests.ElmExtractTests]
ex13 [in ElmExtraction.Tests.ElmExtractTests]
ex2 [in ElmExtraction.Tests.ElmExtractTests]
ex3 [in ElmExtraction.Tests.ElmExtractTests]
ex4 [in ElmExtraction.Tests.ElmExtractTests]
ex5 [in ElmExtraction.Tests.ElmExtractTests]
ex6 [in ElmExtraction.Tests.ElmExtractTests]
ex7 [in ElmExtraction.Tests.ElmExtractTests]
ex8 [in ElmExtraction.Tests.ElmExtractTests]
ex9 [in ElmExtraction.Tests.ElmExtractTests]


P

P [in ElmExtraction.ElmExtract]
P [in ElmExtraction.PrettyPrinterMonad]
PT [in ElmExtraction.ElmExtract]


R

RecordSetNotations [in ElmExtraction.Tests.RecordSet]
recursor_ex [in ElmExtraction.Tests.ElmExtractTests]


T

T [in ElmExtraction.ElmExtract]
TUtil [in ElmExtraction.ElmExtract]
type_scheme_ex.LetouzeyExample [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex [in ElmExtraction.Tests.ElmExtractTests]
T2P [in ElmExtraction.ElmExtract]



Library Index

A

Ack


C

Common


E

ElmExtract
ElmExtractExamples
ElmExtractTests
ElmForms


P

PrettyPrinterMonad


R

RecordSet
RecordUpdate


S

StringExtra



Lemma Index

L

lexicographic_ordering_wf [in ElmExtraction.Tests.Ack]
lt_wf_double_ind [in ElmExtraction.Tests.Ack]
lt_wf_ind [in ElmExtraction.Tests.Ack]


R

recursor_ex.test_is_map [in ElmExtraction.Tests.ElmExtractTests]



Constructor Index

A

Add [in ElmExtraction.Tests.ElmForms]


E

ex8.MPIConstr [in ElmExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr1 [in ElmExtraction.Tests.ElmExtractTests]
ex9.MPINAConstr2 [in ElmExtraction.Tests.ElmExtractTests]


M

MsgName [in ElmExtraction.Tests.ElmForms]
MsgPassword [in ElmExtraction.Tests.ElmForms]
MsgPasswordAgain [in ElmExtraction.Tests.ElmForms]


N

none [in ElmExtraction.Tests.ElmForms]


S

setter_from_getter [in ElmExtraction.Tests.RecordSet]


U

UpdateEntry [in ElmExtraction.Tests.ElmForms]



Inductive Index

C

Cmd [in ElmExtraction.Tests.ElmForms]


E

ex8.ManyParamsInd [in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity [in ElmExtraction.Tests.ElmExtractTests]


M

Msg [in ElmExtraction.Tests.ElmForms]


S

SetterFromGetter [in ElmExtraction.Tests.RecordSet]
StorageMsg [in ElmExtraction.Tests.ElmForms]



Projection Index

A

any_type_symbol [in ElmExtraction.ElmExtract]


C

currentEntry [in ElmExtraction.Tests.ElmForms]
cur_output_line [in ElmExtraction.PrettyPrinterMonad]


E

elmmd_extract [in ElmExtraction.Tests.ElmForms]
errors [in ElmExtraction.Tests.ElmForms]


F

false_elim_def [in ElmExtraction.ElmExtract]


I

indent_stack [in ElmExtraction.PrettyPrinterMonad]


N

name [in ElmExtraction.Tests.ElmForms]


O

output_lines [in ElmExtraction.PrettyPrinterMonad]


P

password [in ElmExtraction.Tests.ElmForms]
passwordAgain [in ElmExtraction.Tests.ElmForms]
print_full_names [in ElmExtraction.ElmExtract]


S

seName [in ElmExtraction.Tests.ElmForms]
sePassword [in ElmExtraction.Tests.ElmForms]
setter_from_getter [in ElmExtraction.Tests.RecordSet]


T

term_box_symbol [in ElmExtraction.ElmExtract]
type_box_symbol [in ElmExtraction.ElmExtract]


U

used_names [in ElmExtraction.PrettyPrinterMonad]
users [in ElmExtraction.Tests.ElmForms]



Instance Index

E

ElmBoxes [in ElmExtraction.Tests.ElmExtractExamples]
ElmBoxes [in ElmExtraction.Tests.ElmForms]


M

Monad_PrettyPrinter [in ElmExtraction.PrettyPrinterMonad]


S

StandardBoxes [in ElmExtraction.Tests.ElmExtractTests]



Section Index

F

FixEnv [in ElmExtraction.ElmExtract]



Abbreviation Index

B

bs_to_s [in ElmExtraction.ElmExtract]
bs_to_s [in ElmExtraction.PrettyPrinterMonad]


S

s_to_bs [in ElmExtraction.ElmExtract]
s_to_bs [in ElmExtraction.PrettyPrinterMonad]



Definition Index

A

ack [in ElmExtraction.Tests.Ack]
append [in ElmExtraction.PrettyPrinterMonad]
append_concat [in ElmExtraction.PrettyPrinterMonad]
append_join [in ElmExtraction.PrettyPrinterMonad]
append_nl [in ElmExtraction.PrettyPrinterMonad]
aRelevant [in ElmExtraction.Tests.RecordSet]


C

capitalize [in ElmExtraction.StringExtra]
char_to_lower [in ElmExtraction.StringExtra]
char_to_upper [in ElmExtraction.StringExtra]
Cmd_sind [in ElmExtraction.Tests.ElmForms]
Cmd_rec [in ElmExtraction.Tests.ElmForms]
Cmd_ind [in ElmExtraction.Tests.ElmForms]
Cmd_rect [in ElmExtraction.Tests.ElmForms]
collect_output [in ElmExtraction.PrettyPrinterMonad]
collect_output_lines [in ElmExtraction.PrettyPrinterMonad]


E

ElmExamples.ackermann [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmExamples_nth [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_foldl [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.ElmList_map [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.head_of_repeat_plus_one [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.inc_counter [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.main_and_test [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.Preambule [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.result_foldl [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.result_map [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.result_nth [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_head [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_partial [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred_full [in ElmExtraction.Tests.ElmExtractExamples]
ElmExamples.safe_pred [in ElmExtraction.Tests.ElmExtractExamples]
elm_false_rec [in ElmExtraction.ElmExtract]
elm_extraction [in ElmExtraction.Tests.ElmForms]
emptyNameError [in ElmExtraction.Tests.ElmForms]
extract [in ElmExtraction.Tests.ElmExtractTests]
extract_def_name_exists [in ElmExtraction.Common]
extract_def_name [in ElmExtraction.Common]
extract_elm_within_coq [in ElmExtraction.Tests.ElmForms]
ex_infix1.test [in ElmExtraction.Tests.ElmExtractTests]
ex_infix1.TT [in ElmExtraction.Tests.ElmExtractTests]
ex1.bar [in ElmExtraction.Tests.ElmExtractTests]
ex1.ex1_test [in ElmExtraction.Tests.ElmExtractTests]
ex1.foo [in ElmExtraction.Tests.ElmExtractTests]
ex10.ex10_test [in ElmExtraction.Tests.ElmExtractTests]
ex10.foo [in ElmExtraction.Tests.ElmExtractTests]
ex11.Monad_test [in ElmExtraction.Tests.ElmExtractTests]
ex12.idT [in ElmExtraction.Tests.ElmExtractTests]
ex12.test [in ElmExtraction.Tests.ElmExtractTests]
ex12.weird_id [in ElmExtraction.Tests.ElmExtractTests]
ex13.opt [in ElmExtraction.Tests.ElmExtractTests]
ex13.test [in ElmExtraction.Tests.ElmExtractTests]
ex13.unwrap [in ElmExtraction.Tests.ElmExtractTests]
ex2.bar [in ElmExtraction.Tests.ElmExtractTests]
ex2.ex2_test [in ElmExtraction.Tests.ElmExtractTests]
ex2.foo [in ElmExtraction.Tests.ElmExtractTests]
ex2.only_in_type [in ElmExtraction.Tests.ElmExtractTests]
ex3.bar [in ElmExtraction.Tests.ElmExtractTests]
ex3.baz [in ElmExtraction.Tests.ElmExtractTests]
ex3.ex3_test [in ElmExtraction.Tests.ElmExtractTests]
ex3.foo [in ElmExtraction.Tests.ElmExtractTests]
ex4.ex4_test [in ElmExtraction.Tests.ElmExtractTests]
ex4.foo [in ElmExtraction.Tests.ElmExtractTests]
ex5.ex5_test [in ElmExtraction.Tests.ElmExtractTests]
ex5.foo [in ElmExtraction.Tests.ElmExtractTests]
ex6.bar [in ElmExtraction.Tests.ElmExtractTests]
ex6.baz [in ElmExtraction.Tests.ElmExtractTests]
ex6.ex6_test [in ElmExtraction.Tests.ElmExtractTests]
ex6.foo [in ElmExtraction.Tests.ElmExtractTests]
ex7.bar [in ElmExtraction.Tests.ElmExtractTests]
ex7.ex7_test [in ElmExtraction.Tests.ElmExtractTests]
ex7.foo [in ElmExtraction.Tests.ElmExtractTests]
ex8.ex8_test [in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_sind [in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rec [in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_ind [in ElmExtraction.Tests.ElmExtractTests]
ex8.ManyParamsInd_rect [in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_test [in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_sind [in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rec [in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_ind [in ElmExtraction.Tests.ElmExtractTests]
ex9.ManyParamsIndNonArity_rect [in ElmExtraction.Tests.ElmExtractTests]


F

finish_print [in ElmExtraction.PrettyPrinterMonad]
finish_print_lines [in ElmExtraction.PrettyPrinterMonad]
fresh [in ElmExtraction.ElmExtract]
fresh_ty_arg_name [in ElmExtraction.ElmExtract]
fresh_ident [in ElmExtraction.ElmExtract]
fresh_name [in ElmExtraction.PrettyPrinterMonad]


G

general_extract [in ElmExtraction.Tests.ElmExtractTests]
general_wrapped [in ElmExtraction.Tests.ElmExtractExamples]
general_wrapped [in ElmExtraction.Tests.ElmForms]
get_infix [in ElmExtraction.ElmExtract]
get_ty_arg_name [in ElmExtraction.ElmExtract]
get_ident_name [in ElmExtraction.ElmExtract]
get_ctor_name [in ElmExtraction.ElmExtract]
get_ty_name [in ElmExtraction.ElmExtract]
get_fun_name [in ElmExtraction.ElmExtract]
get_current_line_length [in ElmExtraction.PrettyPrinterMonad]
get_used_names [in ElmExtraction.PrettyPrinterMonad]
get_indent [in ElmExtraction.PrettyPrinterMonad]


H

header_and_imports [in ElmExtraction.Tests.ElmForms]


I

indent_size [in ElmExtraction.ElmExtract]
initModel [in ElmExtraction.Tests.ElmForms]
is_letter [in ElmExtraction.StringExtra]


L

lexicographic_ordering [in ElmExtraction.Tests.Ack]
lines [in ElmExtraction.StringExtra]
lookup_ind_decl [in ElmExtraction.ElmExtract]
lookup_mind [in ElmExtraction.ElmExtract]


M

make_setters [in ElmExtraction.Tests.RecordSet]
map_cur_output_line [in ElmExtraction.PrettyPrinterMonad]
map_used_names [in ElmExtraction.PrettyPrinterMonad]
map_indent_stack [in ElmExtraction.PrettyPrinterMonad]
map_pps [in ElmExtraction.PrettyPrinterMonad]
monad_append_concat [in ElmExtraction.PrettyPrinterMonad]
monad_append_join [in ElmExtraction.PrettyPrinterMonad]
Msg_sind [in ElmExtraction.Tests.ElmForms]
Msg_rec [in ElmExtraction.Tests.ElmForms]
Msg_ind [in ElmExtraction.Tests.ElmForms]
Msg_rect [in ElmExtraction.Tests.ElmForms]


N

nl [in ElmExtraction.Common]
Nlog2up_nat [in ElmExtraction.StringExtra]
nonEmptyString [in ElmExtraction.Tests.ElmForms]
no_check_args [in ElmExtraction.Tests.ElmExtractTests]
no_check_args [in ElmExtraction.Tests.ElmExtractExamples]


P

parens [in ElmExtraction.Common]
parenthesize_ind_ctor_ty [in ElmExtraction.ElmExtract]
parenthesize_ty_app_arg [in ElmExtraction.ElmExtract]
parenthesize_prod_domain [in ElmExtraction.ElmExtract]
parenthesize_case_branch [in ElmExtraction.ElmExtract]
parenthesize_case_discriminee [in ElmExtraction.ElmExtract]
parenthesize_app_arg [in ElmExtraction.ElmExtract]
parenthesize_app_head [in ElmExtraction.ElmExtract]
passwordIsTooShortError [in ElmExtraction.Tests.ElmForms]
passwordsDoNotMatchError [in ElmExtraction.Tests.ElmForms]
pop_use [in ElmExtraction.PrettyPrinterMonad]
pop_indent [in ElmExtraction.PrettyPrinterMonad]
preamble [in ElmExtraction.Tests.ElmForms]
prefix_spaces [in ElmExtraction.PrettyPrinterMonad]
PrettyPrinter [in ElmExtraction.PrettyPrinterMonad]
printer_fail [in ElmExtraction.PrettyPrinterMonad]
print_env [in ElmExtraction.ElmExtract]
print_type_alias [in ElmExtraction.ElmExtract]
print_mutual_inductive_body [in ElmExtraction.ElmExtract]
print_ind_ctor_definition [in ElmExtraction.ElmExtract]
print_constant [in ElmExtraction.ElmExtract]
print_term [in ElmExtraction.ElmExtract]
print_infix_match_branch [in ElmExtraction.ElmExtract]
print_define_term [in ElmExtraction.ElmExtract]
print_type [in ElmExtraction.ElmExtract]
print_parenthesized [in ElmExtraction.ElmExtract]
print_ind_ctor [in ElmExtraction.ElmExtract]
print_ind [in ElmExtraction.ElmExtract]
push_use [in ElmExtraction.PrettyPrinterMonad]
push_indent [in ElmExtraction.PrettyPrinterMonad]


R

recursor_ex.ex_test [in ElmExtraction.Tests.ElmExtractTests]
recursor_ex.test [in ElmExtraction.Tests.ElmExtractTests]
remap [in ElmExtraction.Common]
remove_char [in ElmExtraction.StringExtra]
replace_char [in ElmExtraction.StringExtra]
result_of_option [in ElmExtraction.Common]
result_of_typing_result [in ElmExtraction.Common]
result_bytestring_err [in ElmExtraction.Tests.ElmExtractTests]
result_string_err [in ElmExtraction.PrettyPrinterMonad]
result_err_bytestring [in ElmExtraction.Tests.ElmExtractExamples]


S

seNames [in ElmExtraction.Tests.ElmForms]
StorageMsg_sind [in ElmExtraction.Tests.ElmForms]
StorageMsg_rec [in ElmExtraction.Tests.ElmForms]
StorageMsg_ind [in ElmExtraction.Tests.ElmForms]
StorageMsg_rect [in ElmExtraction.Tests.ElmForms]
string_of_env_error [in ElmExtraction.Common]
string_of_env_error [in ElmExtraction.PrettyPrinterMonad]
string_of_nat [in ElmExtraction.StringExtra]
string_of_N [in ElmExtraction.StringExtra]
substring_count [in ElmExtraction.StringExtra]
substring_from [in ElmExtraction.StringExtra]


T

toValidStoredEntry [in ElmExtraction.Tests.ElmForms]
to_string_name [in ElmExtraction.Common]
to_globref [in ElmExtraction.Common]
to_kername [in ElmExtraction.Common]
to_inline [in ElmExtraction.Tests.ElmForms]
TT [in ElmExtraction.Tests.ElmForms]
type_scheme_ex.singleton_vec_test [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.singleton_vec [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.vec [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied_test [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_test [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3_applied [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.Sch3 [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.LetouzeyExample.P [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple_test [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Triple [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow_test [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.Arrow [in ElmExtraction.Tests.ElmExtractTests]
type_scheme_ex.general_extract_tc [in ElmExtraction.Tests.ElmExtractTests]


U

uncapitalize [in ElmExtraction.StringExtra]
updateEntry [in ElmExtraction.Tests.ElmForms]
updateModel [in ElmExtraction.Tests.ElmForms]
userAlreadyExistsError [in ElmExtraction.Tests.ElmForms]
USER_FORM_APP [in ElmExtraction.Tests.ElmForms]


V

validateModel [in ElmExtraction.Tests.ElmForms]
ValidEntry [in ElmExtraction.Tests.ElmForms]
validPassword [in ElmExtraction.Tests.ElmForms]
ValidStoredEntry [in ElmExtraction.Tests.ElmForms]


W

wrapped [in ElmExtraction.Tests.ElmExtractExamples]
wrap_result [in ElmExtraction.PrettyPrinterMonad]
wrap_option [in ElmExtraction.PrettyPrinterMonad]
wrap_typing_result [in ElmExtraction.PrettyPrinterMonad]
wrap_EnvCheck [in ElmExtraction.PrettyPrinterMonad]



Record Index

E

ElmMod [in ElmExtraction.Tests.ElmForms]
ElmPrintConfig [in ElmExtraction.ElmExtract]
Entry [in ElmExtraction.Tests.ElmForms]


M

Model [in ElmExtraction.Tests.ElmForms]


P

PrettyPrinterState [in ElmExtraction.PrettyPrinterMonad]


S

SetterFromGetter [in ElmExtraction.Tests.RecordSet]
StoredEntry [in ElmExtraction.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 (311 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 (28 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 (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)
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)
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)
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 (19 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 (1 entry)
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 (206 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 (7 entries)