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 | (305 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 | (10 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) |
| 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]
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]
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
<$ _ ; _ ; .. ; _ $> (bs_scope) [notation, in ElmExtraction.StringExtra]string_literal _ (string_scope) [notation, in ElmExtraction.Tests.ElmForms]
remap_ctor _ of _ to _ [notation, in ElmExtraction.Tests.ElmForms]
<! _ !> [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
<$ _ ; _ ; .. ; _ $> (bs_scope) [in ElmExtraction.StringExtra]string_literal _ (string_scope) [in ElmExtraction.Tests.ElmForms]
remap_ctor _ of _ to _ [in ElmExtraction.Tests.ElmForms]
<! _ !> [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
AckC
CommonE
ElmExtractElmExtractExamples
ElmExtractTests
ElmForms
P
PrettyPrinterMonadR
RecordSetRecordUpdate
S
StringExtraLemma 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]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 | (305 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 | (10 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) |
| 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) |