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 (554 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 (74 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 (26 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 (299 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 (43 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 (15 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 (32 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 (65 entries)

Global Index

A

add_frequency_list_not_in [lemma, in Huffman.Frequency]
add_frequency_list_in [lemma, in Huffman.Frequency]
add_frequency_list_1 [lemma, in Huffman.Frequency]
add_frequency_list_unique_key [lemma, in Huffman.Frequency]
add_frequency_list_in_inv [lemma, in Huffman.Frequency]
add_frequency_list_perm [lemma, in Huffman.Frequency]
add_frequency_list [definition, in Huffman.Frequency]
all_permutations_permutation [lemma, in Huffman.Permutation]
all_permutations_aux_permutation [lemma, in Huffman.Permutation]
all_permutations [definition, in Huffman.Permutation]
all_permutations_aux [definition, in Huffman.Permutation]
all_cover_cover [lemma, in Huffman.Cover]
all_cover_aux_cover [lemma, in Huffman.Cover]
all_cover [definition, in Huffman.Cover]
all_cover_aux [definition, in Huffman.Cover]
all_leaves_ulist [lemma, in Huffman.BTree]
all_leaves_unique [lemma, in Huffman.BTree]
all_leaves_inb [lemma, in Huffman.BTree]
all_leaves_in [lemma, in Huffman.BTree]
all_leaves [definition, in Huffman.BTree]
all_pbleaves_pbbuild [lemma, in Huffman.PBTree]
all_pbleaves_compute_pb [lemma, in Huffman.PBTree]
all_pbleaves_pbleaf [lemma, in Huffman.PBTree]
all_pbleaves_pbadd [lemma, in Huffman.PBTree]
all_pbleaves_ulist [lemma, in Huffman.PBTree]
all_pbleaves_unique [lemma, in Huffman.PBTree]
all_pbleaves_inpb [lemma, in Huffman.PBTree]
all_pbleaves_in [lemma, in Huffman.PBTree]
all_pbleaves [definition, in Huffman.PBTree]
app_inv_app2 [lemma, in Huffman.Aux]
app_inv_app [lemma, in Huffman.Aux]
app_inv_tail [lemma, in Huffman.Aux]
app_inv_head [lemma, in Huffman.Aux]
Aux [library]


B

btree [inductive, in Huffman.BTree]
BTree [library]
btree_unique_prefix [lemma, in Huffman.BTree]
btree_unique_prefix2 [lemma, in Huffman.BTree]
btree_unique_prefix1 [lemma, in Huffman.BTree]
btree_dec [definition, in Huffman.BTree]
build [inductive, in Huffman.Build]
Build [section, in Huffman.Build]
Build [library]
buildf [definition, in Huffman.Build]
build_fun [definition, in Huffman.Build]
build_correct [lemma, in Huffman.Build]
build_permutation [lemma, in Huffman.Build]
build_same_weight_tree [lemma, in Huffman.Build]
build_comp [lemma, in Huffman.Build]
build_cover [lemma, in Huffman.Build]
build_step [constructor, in Huffman.Build]
build_one [constructor, in Huffman.Build]
Build.A [variable, in Huffman.Build]
Build.f [variable, in Huffman.Build]


C

code [definition, in Huffman.Code]
Code [section, in Huffman.Code]
Code [library]
code_dec [definition, in Huffman.Code]
Code.A [variable, in Huffman.Code]
Code.eqA_dec [variable, in Huffman.Code]
compute_code [definition, in Huffman.BTree]
compute_pbcode_not_null [lemma, in Huffman.PBTree]
compute_pbcode [definition, in Huffman.PBTree]
Contradict1 [lemma, in Huffman.sTactic]
Contradict2 [lemma, in Huffman.sTactic]
Contradict3 [lemma, in Huffman.sTactic]
correct_encoding [lemma, in Huffman.Code]
cover [inductive, in Huffman.Cover]
Cover [section, in Huffman.Cover]
Cover [library]
CoverMin [section, in Huffman.CoverMin]
CoverMin [library]
CoverMin.A [variable, in Huffman.CoverMin]
CoverMin.f [variable, in Huffman.CoverMin]
cover_all_leaves [lemma, in Huffman.Cover]
cover_dec [definition, in Huffman.Cover]
cover_all_cover [lemma, in Huffman.Cover]
cover_all_cover_aux [lemma, in Huffman.Cover]
cover_number_of_nodes [lemma, in Huffman.Cover]
cover_app [lemma, in Huffman.Cover]
cover_inv_app [lemma, in Huffman.Cover]
cover_inv_app_aux [lemma, in Huffman.Cover]
cover_one_inv [lemma, in Huffman.Cover]
cover_inv_leaf [lemma, in Huffman.Cover]
cover_inv_leaf_aux [lemma, in Huffman.Cover]
cover_in_inb [lemma, in Huffman.Cover]
cover_in_inb_inb [lemma, in Huffman.Cover]
cover_not_nil [lemma, in Huffman.Cover]
cover_cons_l [lemma, in Huffman.Cover]
cover_permutation [lemma, in Huffman.Cover]
cover_node [constructor, in Huffman.Cover]
cover_one [constructor, in Huffman.Cover]
cover_ordered_cover [lemma, in Huffman.OrderedCover]
cover_min_ex [lemma, in Huffman.CoverMin]
cover_min_permutation [lemma, in Huffman.CoverMin]
cover_min_one [lemma, in Huffman.CoverMin]
cover_min [definition, in Huffman.CoverMin]
Cover.A [variable, in Huffman.Cover]
Cover.empty [variable, in Huffman.Cover]
Cover.eqA_dec [variable, in Huffman.Cover]


D

decode [definition, in Huffman.Code]
decode_correct [lemma, in Huffman.Code]
decode_aux_correct [lemma, in Huffman.Code]
decode_aux [definition, in Huffman.Code]
distinct_leaves_dec [definition, in Huffman.BTree]
distinct_leaves_r [lemma, in Huffman.BTree]
distinct_leaves_l [lemma, in Huffman.BTree]
distinct_leaves_leaf [lemma, in Huffman.BTree]
distinct_leaves [definition, in Huffman.BTree]
distinct_pbleaves_pbadd_prop2 [lemma, in Huffman.PBTree]
distinct_pbleaves_pbadd_prop1 [lemma, in Huffman.PBTree]
distinct_pbleaves_pbright [lemma, in Huffman.PBTree]
distinct_pbleaves_pbleft [lemma, in Huffman.PBTree]
distinct_pbleaves_pbleaf [lemma, in Huffman.PBTree]
distinct_pbleaves_pr [lemma, in Huffman.PBTree]
distinct_pbleaves_pl [lemma, in Huffman.PBTree]
distinct_pbleaves_r [lemma, in Huffman.PBTree]
distinct_pbleaves_l [lemma, in Huffman.PBTree]
distinct_pbleaves_Leaf [lemma, in Huffman.PBTree]
distinct_pbleaves [definition, in Huffman.PBTree]


E

encode [definition, in Huffman.Code]
encode_permutation_val [lemma, in Huffman.Code]
encode_permutation [lemma, in Huffman.Code]
encode_cons_inv [lemma, in Huffman.Code]
encode_app [lemma, in Huffman.Code]
EqBool [section, in Huffman.Aux]
eq_bool_dec [definition, in Huffman.Aux]
exist_first_max [lemma, in Huffman.Aux]
Extraction [library]


F

FindMin [section, in Huffman.Aux]
FindMin.A [variable, in Huffman.Aux]
FindMin.f [variable, in Huffman.Aux]
find_max_correct [lemma, in Huffman.Aux]
find_max [definition, in Huffman.Aux]
find_min_correct [lemma, in Huffman.Aux]
find_min [definition, in Huffman.Aux]
find_val_correct2 [lemma, in Huffman.Code]
find_val_correct1 [lemma, in Huffman.Code]
find_val [definition, in Huffman.Code]
find_code_permutation [lemma, in Huffman.Code]
find_code_app [lemma, in Huffman.Code]
find_code_correct2 [lemma, in Huffman.Code]
find_code_correct1 [lemma, in Huffman.Code]
find_code [definition, in Huffman.Code]
First [section, in Huffman.Aux]
FirstMax [section, in Huffman.Aux]
first_n_skip_n_app [lemma, in Huffman.Aux]
first_n_id [lemma, in Huffman.Aux]
first_n_length [lemma, in Huffman.Aux]
first_n_app2 [lemma, in Huffman.Aux]
first_n_app1 [lemma, in Huffman.Aux]
first_n [definition, in Huffman.Aux]
First.A [variable, in Huffman.Aux]
fold [section, in Huffman.Aux]
fold_left_permutation [lemma, in Huffman.Permutation]
fold_plus_permutation [lemma, in Huffman.Weight]
fold_plus_split [lemma, in Huffman.Weight]
fold_left_init [lemma, in Huffman.Aux]
fold_right_app [lemma, in Huffman.Aux]
fold_left_map [lemma, in Huffman.Aux]
fold_left_eta [lemma, in Huffman.Aux]
fold_left_app [lemma, in Huffman.Aux]
fold_pbadd_prop_node [lemma, in Huffman.PBTree]
fold_pbadd_prop_right [lemma, in Huffman.PBTree]
fold_pbadd_prop_left [lemma, in Huffman.PBTree]
fold.A [variable, in Huffman.Aux]
fold.B [variable, in Huffman.Aux]
fold.eqA_dec [variable, in Huffman.Aux]
fold.f [variable, in Huffman.Aux]
fold.g [variable, in Huffman.Aux]
fold.h [variable, in Huffman.Aux]
Frequency [section, in Huffman.Frequency]
Frequency [library]
frequency_list_restric_code_map [lemma, in Huffman.Restrict]
frequency_length [lemma, in Huffman.Weight]
frequency_not_null [lemma, in Huffman.Code]
frequency_number_of_occurrences [lemma, in Huffman.Frequency]
frequency_list_unique [lemma, in Huffman.Frequency]
frequency_list_perm [lemma, in Huffman.Frequency]
frequency_list_in [lemma, in Huffman.Frequency]
frequency_list [definition, in Huffman.Frequency]
Frequency.A [variable, in Huffman.Frequency]
Frequency.eqA_dec [variable, in Huffman.Frequency]


H

HeightPred [section, in Huffman.HeightPred]
HeightPred [library]
HeightPred.A [variable, in Huffman.HeightPred]
HeightPred.eqA_dec [variable, in Huffman.HeightPred]
HeightPred.f [variable, in Huffman.HeightPred]
height_pred_compute_code [lemma, in Huffman.HeightPred]
height_pred_shrink [lemma, in Huffman.HeightPred]
height_pred_shrink_aux [lemma, in Huffman.HeightPred]
height_pred_disj_larger2 [lemma, in Huffman.HeightPred]
height_pred_disj_larger2_aux [lemma, in Huffman.HeightPred]
height_pred_disj_larger [lemma, in Huffman.HeightPred]
height_pred_disj_larger_aux [lemma, in Huffman.HeightPred]
height_pred_larger_ex [lemma, in Huffman.HeightPred]
height_pred_larger_strict [lemma, in Huffman.HeightPred]
height_pred_larger [lemma, in Huffman.HeightPred]
height_pred_weight [lemma, in Huffman.HeightPred]
height_pred_length [lemma, in Huffman.HeightPred]
height_pred_not_nil2 [lemma, in Huffman.HeightPred]
height_pred_not_nil1 [lemma, in Huffman.HeightPred]
height_pred_ordered_cover [lemma, in Huffman.HeightPred]
height_pred_node [constructor, in Huffman.HeightPred]
height_pred_nil [constructor, in Huffman.HeightPred]
height_pred [inductive, in Huffman.HeightPred]
height_pred_subst_pred [lemma, in Huffman.SubstPred]
huffman [definition, in Huffman.Huffman]
Huffman [section, in Huffman.Huffman]
Huffman [library]
huffman_aux [definition, in Huffman.Huffman]
huffman_build_minimun [lemma, in Huffman.Huffman]
Huffman.A [variable, in Huffman.Huffman]
Huffman.empty [variable, in Huffman.Huffman]
Huffman.eqA_dec [variable, in Huffman.Huffman]
Huffman.frequency_more_than_one [variable, in Huffman.Huffman]
Huffman.m [variable, in Huffman.Huffman]


I

id_list [definition, in Huffman.Frequency]
inb [inductive, in Huffman.BTree]
inb_compute_ex [lemma, in Huffman.BTree]
inb_dec [definition, in Huffman.BTree]
inb_antisym [lemma, in Huffman.BTree]
inb_ex [lemma, in Huffman.BTree]
inb_trans [lemma, in Huffman.BTree]
inCompute_inb [lemma, in Huffman.BTree]
inleaf [constructor, in Huffman.BTree]
innodeL [constructor, in Huffman.BTree]
innodeR [constructor, in Huffman.BTree]
inpb [inductive, in Huffman.PBTree]
inpbleaf_pbadd_inv [lemma, in Huffman.PBTree]
inpbleaf_eq [lemma, in Huffman.PBTree]
inpb_pbbuild_inv [lemma, in Huffman.PBTree]
inpb_pbadd_ex [lemma, in Huffman.PBTree]
inpb_pbadd [lemma, in Huffman.PBTree]
inpb_compute_ex [lemma, in Huffman.PBTree]
inpb_ex [lemma, in Huffman.PBTree]
inpb_trans [lemma, in Huffman.PBTree]
inpb_dec [definition, in Huffman.PBTree]
inpb_node_r [constructor, in Huffman.PBTree]
inpb_node_l [constructor, in Huffman.PBTree]
inpb_right [constructor, in Huffman.PBTree]
inpb_left [constructor, in Huffman.PBTree]
inpb_leaf [constructor, in Huffman.PBTree]
insert [definition, in Huffman.ISort]
insert_permutation [lemma, in Huffman.ISort]
insert_ordered [lemma, in Huffman.ISort]
in_permutation_ex [lemma, in Huffman.Permutation]
in_alphabet_compute_code [lemma, in Huffman.BTree]
in_flat_map_ex [lemma, in Huffman.Aux]
in_flat_map [lemma, in Huffman.Aux]
in_map_fst_inv [lemma, in Huffman.Aux]
in_map_inv [lemma, in Huffman.Aux]
in_ex_app [lemma, in Huffman.Aux]
in_pbleaf_node [lemma, in Huffman.PBTree]
in_pbcompute_inpb [lemma, in Huffman.PBTree]
in_find_map [lemma, in Huffman.Code]
in_alphabet_dec [definition, in Huffman.Code]
in_alphabet_inv [lemma, in Huffman.Code]
in_alphabet_cons [lemma, in Huffman.Code]
in_alphabet_nil [lemma, in Huffman.Code]
in_alphabet_incl [lemma, in Huffman.Code]
in_alphabet [definition, in Huffman.Code]
in_frequency_map_inv [lemma, in Huffman.Frequency]
in_frequency_map [lemma, in Huffman.Frequency]
isort [definition, in Huffman.ISort]
ISort [library]
ISortExample [section, in Huffman.ISort]
ISortExample.A [variable, in Huffman.ISort]
ISortExample.order [variable, in Huffman.ISort]
ISortExample.order_fun_false [variable, in Huffman.ISort]
ISortExample.order_fun_true [variable, in Huffman.ISort]
ISortExample.order_fun [variable, in Huffman.ISort]
isort_permutation [lemma, in Huffman.ISort]
isort_ordered [lemma, in Huffman.ISort]
is_prefix_refl [lemma, in Huffman.Code]
is_prefix [inductive, in Huffman.Code]


L

leaf [constructor, in Huffman.BTree]
LeBool [section, in Huffman.Aux]
length_compute_lt_O [lemma, in Huffman.BTree]
length_encode_nId [lemma, in Huffman.Weight]
length_map [lemma, in Huffman.Aux]
length_app [lemma, in Huffman.Aux]
le_sum_correct2 [lemma, in Huffman.WeightTree]
le_sum_correct1 [lemma, in Huffman.WeightTree]
le_sum [definition, in Huffman.WeightTree]
le_bool_correct4 [lemma, in Huffman.Aux]
le_bool_correct3 [lemma, in Huffman.Aux]
le_bool_correct2 [lemma, in Huffman.Aux]
le_bool_correct1 [lemma, in Huffman.Aux]
le_bool [definition, in Huffman.Aux]
le_minus [lemma, in Huffman.Aux]
List [section, in Huffman.Aux]
list_length_induction [definition, in Huffman.Aux]
list_length_ind [lemma, in Huffman.Aux]
List.A [variable, in Huffman.Aux]
List.B [variable, in Huffman.Aux]
List.C [variable, in Huffman.Aux]
List.f [variable, in Huffman.Aux]
lt_minus_O [lemma, in Huffman.Aux]


M

map_app [lemma, in Huffman.Aux]
map2 [definition, in Huffman.Aux]
map2 [section, in Huffman.Aux]
map2_app [lemma, in Huffman.Aux]
map2.A [variable, in Huffman.Aux]
map2.B [variable, in Huffman.Aux]
map2.C [variable, in Huffman.Aux]
map2.f [variable, in Huffman.Aux]
Minus [section, in Huffman.Aux]
minus_minus_simpl4 [lemma, in Huffman.Aux]


N

node [constructor, in Huffman.BTree]
not_null_m [lemma, in Huffman.Huffman]
not_null_find_val [lemma, in Huffman.Code]
not_in_find_map [lemma, in Huffman.Code]
not_in_find_code [lemma, in Huffman.Code]
not_null_map [lemma, in Huffman.Code]
not_null_app [lemma, in Huffman.Code]
not_null_cons [lemma, in Huffman.Code]
not_null_inv [lemma, in Huffman.Code]
not_null [definition, in Huffman.Code]
number_of_nodes_inb_le [lemma, in Huffman.BTree]
number_of_nodes [definition, in Huffman.BTree]
number_of_occurrences_permutation [lemma, in Huffman.Frequency]
number_of_occurrences_app [lemma, in Huffman.Frequency]
number_of_occurrences_permutation_ex [lemma, in Huffman.Frequency]
number_of_occurrences_O [lemma, in Huffman.Frequency]
number_of_occurrences [definition, in Huffman.Frequency]


O

obuildf [definition, in Huffman.Build]
OneStep [section, in Huffman.OneStep]
OneStep [library]
OneStep.A [variable, in Huffman.OneStep]
OneStep.f [variable, in Huffman.OneStep]
one_cover_ex [lemma, in Huffman.Cover]
one_step_comp [lemma, in Huffman.OneStep]
one_step_same_sum_leaves [lemma, in Huffman.OneStep]
one_step_weight_tree_list [lemma, in Huffman.OneStep]
one_step [definition, in Huffman.OneStep]
ordered [inductive, in Huffman.Ordered]
ordered [section, in Huffman.Ordered]
Ordered [library]
OrderedCover [section, in Huffman.OrderedCover]
OrderedCover [library]
OrderedCover.A [variable, in Huffman.OrderedCover]
ordered_sum_leaves_eq [lemma, in Huffman.WeightTree]
ordered_cover_cover [lemma, in Huffman.OrderedCover]
ordered_cover_node [constructor, in Huffman.OrderedCover]
ordered_cover_one [constructor, in Huffman.OrderedCover]
ordered_cover [inductive, in Huffman.OrderedCover]
ordered_map_inv [lemma, in Huffman.Ordered]
ordered_perm_antisym_eq [lemma, in Huffman.Ordered]
ordered_trans_app [lemma, in Huffman.Ordered]
ordered_trans [lemma, in Huffman.Ordered]
ordered_skip [lemma, in Huffman.Ordered]
ordered_inv [lemma, in Huffman.Ordered]
ordered_inv_order [lemma, in Huffman.Ordered]
ordered_cons [constructor, in Huffman.Ordered]
ordered_one [constructor, in Huffman.Ordered]
ordered_nil [constructor, in Huffman.Ordered]
ordered_cover_height_pred [lemma, in Huffman.HeightPred]
ordered_cover_subst_pred [lemma, in Huffman.SubstPred]
ordered.A [variable, in Huffman.Ordered]
ordered.order [variable, in Huffman.Ordered]
ordered.order_trans [variable, in Huffman.Ordered]


P

pbadd [definition, in Huffman.PBTree]
pbadd_prop2 [lemma, in Huffman.PBTree]
pbadd_prop1 [lemma, in Huffman.PBTree]
pbbuild [definition, in Huffman.PBTree]
pbbuild_pbnode [lemma, in Huffman.PBTree]
pbbuild_true_pbright [lemma, in Huffman.PBTree]
pbbuild_compute_peq [lemma, in Huffman.PBTree]
pbbuild_distinct_pbleaves [lemma, in Huffman.PBTree]
pbbuild_compute_perm [lemma, in Huffman.PBTree]
pbfree [inductive, in Huffman.PBTree]
pbfree_pbbuild_prop1 [lemma, in Huffman.PBTree]
pbfree_pbadd_prop2 [lemma, in Huffman.PBTree]
pbfree_pbadd_prop1 [lemma, in Huffman.PBTree]
pbfree_node2 [constructor, in Huffman.PBTree]
pbfree_node1 [constructor, in Huffman.PBTree]
pbfree_right2 [constructor, in Huffman.PBTree]
pbfree_right1 [constructor, in Huffman.PBTree]
pbfree_left2 [constructor, in Huffman.PBTree]
pbfree_left1 [constructor, in Huffman.PBTree]
pbleaf [constructor, in Huffman.PBTree]
pbleaf_or_not [lemma, in Huffman.PBTree]
pbleft [constructor, in Huffman.PBTree]
pbnode [constructor, in Huffman.PBTree]
pbright [constructor, in Huffman.PBTree]
pbtree [inductive, in Huffman.PBTree]
PBTree [section, in Huffman.PBTree]
PBTree [library]
pbtree_dec [definition, in Huffman.PBTree]
PBTree.A [variable, in Huffman.PBTree]
PBTree.empty [variable, in Huffman.PBTree]
PBTree.eqA_dec [variable, in Huffman.PBTree]
PBTREE2BTREE [section, in Huffman.PBTree2BTree]
PBTree2BTree [library]
PBTREE2BTREE.A [variable, in Huffman.PBTree2BTree]
PBTREE2BTREE.empty [variable, in Huffman.PBTree2BTree]
PBTREE2BTREE.eqA_dec [variable, in Huffman.PBTree2BTree]
pb_unique_prefix [lemma, in Huffman.PBTree]
pb_unique_key [lemma, in Huffman.PBTree]
pb_unique_prefix1 [lemma, in Huffman.PBTree]
permutation [inductive, in Huffman.Permutation]
permutation [section, in Huffman.Permutation]
Permutation [library]
permutation_flat_map [lemma, in Huffman.Permutation]
permutation_map_ex [lemma, in Huffman.Permutation]
permutation_map_ex_aux [lemma, in Huffman.Permutation]
permutation_map [lemma, in Huffman.Permutation]
permutation_dec [definition, in Huffman.Permutation]
permutation_all_permutations [lemma, in Huffman.Permutation]
permutation_all_permutations_aux [lemma, in Huffman.Permutation]
permutation_inv [lemma, in Huffman.Permutation]
permutation_cons_ex [lemma, in Huffman.Permutation]
permutation_cons_ex_aux [lemma, in Huffman.Permutation]
permutation_transposition [lemma, in Huffman.Permutation]
permutation_app_swap [lemma, in Huffman.Permutation]
permutation_app_comp [lemma, in Huffman.Permutation]
permutation_in [lemma, in Huffman.Permutation]
permutation_one_inv [lemma, in Huffman.Permutation]
permutation_one_inv_aux [lemma, in Huffman.Permutation]
permutation_nil_inv [lemma, in Huffman.Permutation]
permutation_length [lemma, in Huffman.Permutation]
permutation_sym [lemma, in Huffman.Permutation]
permutation_refl [lemma, in Huffman.Permutation]
permutation_trans [constructor, in Huffman.Permutation]
permutation_swap [constructor, in Huffman.Permutation]
permutation_skip [constructor, in Huffman.Permutation]
permutation_nil [constructor, in Huffman.Permutation]
permutation.A [variable, in Huffman.Permutation]
plus_minus_simpl4 [lemma, in Huffman.Aux]
prefixCons [constructor, in Huffman.Code]
prefixNull [constructor, in Huffman.Code]
prod2list [definition, in Huffman.Prod2List]
Prod2List [section, in Huffman.Prod2List]
Prod2List [library]
prod2list_reorder2 [lemma, in Huffman.Prod2List]
prod2list_reorder [lemma, in Huffman.Prod2List]
prod2list_eq [lemma, in Huffman.Prod2List]
prod2list_le_r [lemma, in Huffman.Prod2List]
prod2list_le_l [lemma, in Huffman.Prod2List]
prod2list_app [lemma, in Huffman.Prod2List]
Prod2List.A [variable, in Huffman.Prod2List]
Prod2List.f [variable, in Huffman.Prod2List]


R

Restrict [section, in Huffman.Restrict]
Restrict [library]
restrict_code_pbbuild [lemma, in Huffman.Restrict]
restrict_not_null [lemma, in Huffman.Restrict]
restrict_unique_prefix [lemma, in Huffman.Restrict]
restrict_code_encode [lemma, in Huffman.Restrict]
restrict_code_encode_incl [lemma, in Huffman.Restrict]
restrict_code_in [lemma, in Huffman.Restrict]
restrict_code_unique_key [lemma, in Huffman.Restrict]
restrict_code [definition, in Huffman.Restrict]
restrict_code_encode_length [lemma, in Huffman.Weight]
restrict_code_encode_length_inc [lemma, in Huffman.Weight]
restrict_code_in [lemma, in Huffman.Weight]
restrict_code_unique_key [lemma, in Huffman.Weight]
restrict_code [definition, in Huffman.Weight]
Restrict.A [variable, in Huffman.Restrict]
Restrict.empty [variable, in Huffman.Restrict]
Restrict.eqA_dec [variable, in Huffman.Restrict]
Restrict.m [variable, in Huffman.Restrict]


S

SameSumLeaves [section, in Huffman.SameSumLeaves]
SameSumLeaves [library]
SameSumLeaves.A [variable, in Huffman.SameSumLeaves]
SameSumLeaves.f [variable, in Huffman.SameSumLeaves]
same_length_ex [lemma, in Huffman.Aux]
same_sum_leaves_length [lemma, in Huffman.SameSumLeaves]
same_sum_leaves [definition, in Huffman.SameSumLeaves]
skip_n_id [lemma, in Huffman.Aux]
skip_n_length [lemma, in Huffman.Aux]
skip_n_app2 [lemma, in Huffman.Aux]
skip_n_app1 [lemma, in Huffman.Aux]
skip_n [definition, in Huffman.Aux]
split_one_in_ex [lemma, in Huffman.Permutation]
split_one_permutation [lemma, in Huffman.Permutation]
split_one [definition, in Huffman.Permutation]
sTactic [library]
SubstPred [section, in Huffman.SubstPred]
SubstPred [library]
SubstPred.A [variable, in Huffman.SubstPred]
subst_pred_length [lemma, in Huffman.SubstPred]
subst_pred_ordered_cover_r [lemma, in Huffman.SubstPred]
subst_pred_ordered_cover_l [lemma, in Huffman.SubstPred]
subst_pred_node [constructor, in Huffman.SubstPred]
subst_pred_id [constructor, in Huffman.SubstPred]
subst_pred [inductive, in Huffman.SubstPred]
sum_order [definition, in Huffman.WeightTree]
sum_leaves [definition, in Huffman.WeightTree]


T

to_btree_smaller [lemma, in Huffman.PBTree2BTree]
to_btree_distinct_pbleaves [lemma, in Huffman.PBTree2BTree]
to_btree_distinct_leaves [lemma, in Huffman.PBTree2BTree]
to_btree_all_leaves [lemma, in Huffman.PBTree2BTree]
to_btree_inpb [lemma, in Huffman.PBTree2BTree]
to_btree_inb [lemma, in Huffman.PBTree2BTree]
to_btree [definition, in Huffman.PBTree2BTree]
Tree [section, in Huffman.BTree]
Tree.A [variable, in Huffman.BTree]
Tree.empty [variable, in Huffman.BTree]
Tree.eqA_dec [variable, in Huffman.BTree]


U

ulist [inductive, in Huffman.UList]
UList [library]
ulist_unique_key [lemma, in Huffman.Weight]
ulist_ordered_cover [lemma, in Huffman.OrderedCover]
ulist_pbadd_prop2 [lemma, in Huffman.PBTree]
ulist_unique_key [lemma, in Huffman.UniqueKey]
ulist_perm [lemma, in Huffman.UList]
ulist_dec [definition, in Huffman.UList]
ulist_app_inv_r [lemma, in Huffman.UList]
ulist_app_inv_l [lemma, in Huffman.UList]
ulist_app_inv [lemma, in Huffman.UList]
ulist_app [lemma, in Huffman.UList]
ulist_inv [lemma, in Huffman.UList]
ulist_cons [constructor, in Huffman.UList]
ulist_nil [constructor, in Huffman.UList]
UniqueKey [section, in Huffman.UniqueKey]
UniqueKey [library]
UniqueKey.A [variable, in Huffman.UniqueKey]
UniqueKey.B [variable, in Huffman.UniqueKey]
UniqueList [section, in Huffman.UList]
UniqueList.A [variable, in Huffman.UList]
UniqueList.eqA_dec [variable, in Huffman.UList]
unique_key_map [lemma, in Huffman.UniqueKey]
unique_key_ulist [lemma, in Huffman.UniqueKey]
unique_key_app [lemma, in Huffman.UniqueKey]
unique_key_perm [lemma, in Huffman.UniqueKey]
unique_key_in_inv [lemma, in Huffman.UniqueKey]
unique_key_in [lemma, in Huffman.UniqueKey]
unique_key_inv [lemma, in Huffman.UniqueKey]
unique_key_cons [constructor, in Huffman.UniqueKey]
unique_key_nil [constructor, in Huffman.UniqueKey]
unique_key [inductive, in Huffman.UniqueKey]
unique_prefix_permutation [lemma, in Huffman.Code]
unique_prefix_not_null [lemma, in Huffman.Code]
unique_prefix_inv [lemma, in Huffman.Code]
unique_prefix2 [lemma, in Huffman.Code]
unique_prefix1 [lemma, in Huffman.Code]
unique_prefix_nil [lemma, in Huffman.Code]
unique_prefix [definition, in Huffman.Code]


W

weight [definition, in Huffman.Weight]
Weight [section, in Huffman.Weight]
Weight [library]
WeightTree [section, in Huffman.WeightTree]
WeightTree [library]
WeightTree.A [variable, in Huffman.WeightTree]
WeightTree.f [variable, in Huffman.WeightTree]
weight_tree_list_permutation [lemma, in Huffman.WeightTree]
weight_tree_list_node [lemma, in Huffman.WeightTree]
weight_tree_list [definition, in Huffman.WeightTree]
weight_tree [definition, in Huffman.WeightTree]
weight_permutation [lemma, in Huffman.Weight]
weight_tree_compute [lemma, in Huffman.HeightPred]
Weight.A [variable, in Huffman.Weight]
Weight.eqA_dec [variable, in Huffman.Weight]



Variable Index

B

Build.A [in Huffman.Build]
Build.f [in Huffman.Build]


C

Code.A [in Huffman.Code]
Code.eqA_dec [in Huffman.Code]
CoverMin.A [in Huffman.CoverMin]
CoverMin.f [in Huffman.CoverMin]
Cover.A [in Huffman.Cover]
Cover.empty [in Huffman.Cover]
Cover.eqA_dec [in Huffman.Cover]


F

FindMin.A [in Huffman.Aux]
FindMin.f [in Huffman.Aux]
First.A [in Huffman.Aux]
fold.A [in Huffman.Aux]
fold.B [in Huffman.Aux]
fold.eqA_dec [in Huffman.Aux]
fold.f [in Huffman.Aux]
fold.g [in Huffman.Aux]
fold.h [in Huffman.Aux]
Frequency.A [in Huffman.Frequency]
Frequency.eqA_dec [in Huffman.Frequency]


H

HeightPred.A [in Huffman.HeightPred]
HeightPred.eqA_dec [in Huffman.HeightPred]
HeightPred.f [in Huffman.HeightPred]
Huffman.A [in Huffman.Huffman]
Huffman.empty [in Huffman.Huffman]
Huffman.eqA_dec [in Huffman.Huffman]
Huffman.frequency_more_than_one [in Huffman.Huffman]
Huffman.m [in Huffman.Huffman]


I

ISortExample.A [in Huffman.ISort]
ISortExample.order [in Huffman.ISort]
ISortExample.order_fun_false [in Huffman.ISort]
ISortExample.order_fun_true [in Huffman.ISort]
ISortExample.order_fun [in Huffman.ISort]


L

List.A [in Huffman.Aux]
List.B [in Huffman.Aux]
List.C [in Huffman.Aux]
List.f [in Huffman.Aux]


M

map2.A [in Huffman.Aux]
map2.B [in Huffman.Aux]
map2.C [in Huffman.Aux]
map2.f [in Huffman.Aux]


O

OneStep.A [in Huffman.OneStep]
OneStep.f [in Huffman.OneStep]
OrderedCover.A [in Huffman.OrderedCover]
ordered.A [in Huffman.Ordered]
ordered.order [in Huffman.Ordered]
ordered.order_trans [in Huffman.Ordered]


P

PBTree.A [in Huffman.PBTree]
PBTree.empty [in Huffman.PBTree]
PBTree.eqA_dec [in Huffman.PBTree]
PBTREE2BTREE.A [in Huffman.PBTree2BTree]
PBTREE2BTREE.empty [in Huffman.PBTree2BTree]
PBTREE2BTREE.eqA_dec [in Huffman.PBTree2BTree]
permutation.A [in Huffman.Permutation]
Prod2List.A [in Huffman.Prod2List]
Prod2List.f [in Huffman.Prod2List]


R

Restrict.A [in Huffman.Restrict]
Restrict.empty [in Huffman.Restrict]
Restrict.eqA_dec [in Huffman.Restrict]
Restrict.m [in Huffman.Restrict]


S

SameSumLeaves.A [in Huffman.SameSumLeaves]
SameSumLeaves.f [in Huffman.SameSumLeaves]
SubstPred.A [in Huffman.SubstPred]


T

Tree.A [in Huffman.BTree]
Tree.empty [in Huffman.BTree]
Tree.eqA_dec [in Huffman.BTree]


U

UniqueKey.A [in Huffman.UniqueKey]
UniqueKey.B [in Huffman.UniqueKey]
UniqueList.A [in Huffman.UList]
UniqueList.eqA_dec [in Huffman.UList]


W

WeightTree.A [in Huffman.WeightTree]
WeightTree.f [in Huffman.WeightTree]
Weight.A [in Huffman.Weight]
Weight.eqA_dec [in Huffman.Weight]



Library Index

A

Aux


B

BTree
Build


C

Code
Cover
CoverMin


E

Extraction


F

Frequency


H

HeightPred
Huffman


I

ISort


O

OneStep
Ordered
OrderedCover


P

PBTree
PBTree2BTree
Permutation
Prod2List


R

Restrict


S

SameSumLeaves
sTactic
SubstPred


U

UList
UniqueKey


W

Weight
WeightTree



Lemma Index

A

add_frequency_list_not_in [in Huffman.Frequency]
add_frequency_list_in [in Huffman.Frequency]
add_frequency_list_1 [in Huffman.Frequency]
add_frequency_list_unique_key [in Huffman.Frequency]
add_frequency_list_in_inv [in Huffman.Frequency]
add_frequency_list_perm [in Huffman.Frequency]
all_permutations_permutation [in Huffman.Permutation]
all_permutations_aux_permutation [in Huffman.Permutation]
all_cover_cover [in Huffman.Cover]
all_cover_aux_cover [in Huffman.Cover]
all_leaves_ulist [in Huffman.BTree]
all_leaves_unique [in Huffman.BTree]
all_leaves_inb [in Huffman.BTree]
all_leaves_in [in Huffman.BTree]
all_pbleaves_pbbuild [in Huffman.PBTree]
all_pbleaves_compute_pb [in Huffman.PBTree]
all_pbleaves_pbleaf [in Huffman.PBTree]
all_pbleaves_pbadd [in Huffman.PBTree]
all_pbleaves_ulist [in Huffman.PBTree]
all_pbleaves_unique [in Huffman.PBTree]
all_pbleaves_inpb [in Huffman.PBTree]
all_pbleaves_in [in Huffman.PBTree]
app_inv_app2 [in Huffman.Aux]
app_inv_app [in Huffman.Aux]
app_inv_tail [in Huffman.Aux]
app_inv_head [in Huffman.Aux]


B

btree_unique_prefix [in Huffman.BTree]
btree_unique_prefix2 [in Huffman.BTree]
btree_unique_prefix1 [in Huffman.BTree]
build_correct [in Huffman.Build]
build_permutation [in Huffman.Build]
build_same_weight_tree [in Huffman.Build]
build_comp [in Huffman.Build]
build_cover [in Huffman.Build]


C

compute_pbcode_not_null [in Huffman.PBTree]
Contradict1 [in Huffman.sTactic]
Contradict2 [in Huffman.sTactic]
Contradict3 [in Huffman.sTactic]
correct_encoding [in Huffman.Code]
cover_all_leaves [in Huffman.Cover]
cover_all_cover [in Huffman.Cover]
cover_all_cover_aux [in Huffman.Cover]
cover_number_of_nodes [in Huffman.Cover]
cover_app [in Huffman.Cover]
cover_inv_app [in Huffman.Cover]
cover_inv_app_aux [in Huffman.Cover]
cover_one_inv [in Huffman.Cover]
cover_inv_leaf [in Huffman.Cover]
cover_inv_leaf_aux [in Huffman.Cover]
cover_in_inb [in Huffman.Cover]
cover_in_inb_inb [in Huffman.Cover]
cover_not_nil [in Huffman.Cover]
cover_cons_l [in Huffman.Cover]
cover_permutation [in Huffman.Cover]
cover_ordered_cover [in Huffman.OrderedCover]
cover_min_ex [in Huffman.CoverMin]
cover_min_permutation [in Huffman.CoverMin]
cover_min_one [in Huffman.CoverMin]


D

decode_correct [in Huffman.Code]
decode_aux_correct [in Huffman.Code]
distinct_leaves_r [in Huffman.BTree]
distinct_leaves_l [in Huffman.BTree]
distinct_leaves_leaf [in Huffman.BTree]
distinct_pbleaves_pbadd_prop2 [in Huffman.PBTree]
distinct_pbleaves_pbadd_prop1 [in Huffman.PBTree]
distinct_pbleaves_pbright [in Huffman.PBTree]
distinct_pbleaves_pbleft [in Huffman.PBTree]
distinct_pbleaves_pbleaf [in Huffman.PBTree]
distinct_pbleaves_pr [in Huffman.PBTree]
distinct_pbleaves_pl [in Huffman.PBTree]
distinct_pbleaves_r [in Huffman.PBTree]
distinct_pbleaves_l [in Huffman.PBTree]
distinct_pbleaves_Leaf [in Huffman.PBTree]


E

encode_permutation_val [in Huffman.Code]
encode_permutation [in Huffman.Code]
encode_cons_inv [in Huffman.Code]
encode_app [in Huffman.Code]
exist_first_max [in Huffman.Aux]


F

find_max_correct [in Huffman.Aux]
find_min_correct [in Huffman.Aux]
find_val_correct2 [in Huffman.Code]
find_val_correct1 [in Huffman.Code]
find_code_permutation [in Huffman.Code]
find_code_app [in Huffman.Code]
find_code_correct2 [in Huffman.Code]
find_code_correct1 [in Huffman.Code]
first_n_skip_n_app [in Huffman.Aux]
first_n_id [in Huffman.Aux]
first_n_length [in Huffman.Aux]
first_n_app2 [in Huffman.Aux]
first_n_app1 [in Huffman.Aux]
fold_left_permutation [in Huffman.Permutation]
fold_plus_permutation [in Huffman.Weight]
fold_plus_split [in Huffman.Weight]
fold_left_init [in Huffman.Aux]
fold_right_app [in Huffman.Aux]
fold_left_map [in Huffman.Aux]
fold_left_eta [in Huffman.Aux]
fold_left_app [in Huffman.Aux]
fold_pbadd_prop_node [in Huffman.PBTree]
fold_pbadd_prop_right [in Huffman.PBTree]
fold_pbadd_prop_left [in Huffman.PBTree]
frequency_list_restric_code_map [in Huffman.Restrict]
frequency_length [in Huffman.Weight]
frequency_not_null [in Huffman.Code]
frequency_number_of_occurrences [in Huffman.Frequency]
frequency_list_unique [in Huffman.Frequency]
frequency_list_perm [in Huffman.Frequency]
frequency_list_in [in Huffman.Frequency]


H

height_pred_compute_code [in Huffman.HeightPred]
height_pred_shrink [in Huffman.HeightPred]
height_pred_shrink_aux [in Huffman.HeightPred]
height_pred_disj_larger2 [in Huffman.HeightPred]
height_pred_disj_larger2_aux [in Huffman.HeightPred]
height_pred_disj_larger [in Huffman.HeightPred]
height_pred_disj_larger_aux [in Huffman.HeightPred]
height_pred_larger_ex [in Huffman.HeightPred]
height_pred_larger_strict [in Huffman.HeightPred]
height_pred_larger [in Huffman.HeightPred]
height_pred_weight [in Huffman.HeightPred]
height_pred_length [in Huffman.HeightPred]
height_pred_not_nil2 [in Huffman.HeightPred]
height_pred_not_nil1 [in Huffman.HeightPred]
height_pred_ordered_cover [in Huffman.HeightPred]
height_pred_subst_pred [in Huffman.SubstPred]
huffman_build_minimun [in Huffman.Huffman]


I

inb_compute_ex [in Huffman.BTree]
inb_antisym [in Huffman.BTree]
inb_ex [in Huffman.BTree]
inb_trans [in Huffman.BTree]
inCompute_inb [in Huffman.BTree]
inpbleaf_pbadd_inv [in Huffman.PBTree]
inpbleaf_eq [in Huffman.PBTree]
inpb_pbbuild_inv [in Huffman.PBTree]
inpb_pbadd_ex [in Huffman.PBTree]
inpb_pbadd [in Huffman.PBTree]
inpb_compute_ex [in Huffman.PBTree]
inpb_ex [in Huffman.PBTree]
inpb_trans [in Huffman.PBTree]
insert_permutation [in Huffman.ISort]
insert_ordered [in Huffman.ISort]
in_permutation_ex [in Huffman.Permutation]
in_alphabet_compute_code [in Huffman.BTree]
in_flat_map_ex [in Huffman.Aux]
in_flat_map [in Huffman.Aux]
in_map_fst_inv [in Huffman.Aux]
in_map_inv [in Huffman.Aux]
in_ex_app [in Huffman.Aux]
in_pbleaf_node [in Huffman.PBTree]
in_pbcompute_inpb [in Huffman.PBTree]
in_find_map [in Huffman.Code]
in_alphabet_inv [in Huffman.Code]
in_alphabet_cons [in Huffman.Code]
in_alphabet_nil [in Huffman.Code]
in_alphabet_incl [in Huffman.Code]
in_frequency_map_inv [in Huffman.Frequency]
in_frequency_map [in Huffman.Frequency]
isort_permutation [in Huffman.ISort]
isort_ordered [in Huffman.ISort]
is_prefix_refl [in Huffman.Code]


L

length_compute_lt_O [in Huffman.BTree]
length_encode_nId [in Huffman.Weight]
length_map [in Huffman.Aux]
length_app [in Huffman.Aux]
le_sum_correct2 [in Huffman.WeightTree]
le_sum_correct1 [in Huffman.WeightTree]
le_bool_correct4 [in Huffman.Aux]
le_bool_correct3 [in Huffman.Aux]
le_bool_correct2 [in Huffman.Aux]
le_bool_correct1 [in Huffman.Aux]
le_minus [in Huffman.Aux]
list_length_ind [in Huffman.Aux]
lt_minus_O [in Huffman.Aux]


M

map_app [in Huffman.Aux]
map2_app [in Huffman.Aux]
minus_minus_simpl4 [in Huffman.Aux]


N

not_null_m [in Huffman.Huffman]
not_null_find_val [in Huffman.Code]
not_in_find_map [in Huffman.Code]
not_in_find_code [in Huffman.Code]
not_null_map [in Huffman.Code]
not_null_app [in Huffman.Code]
not_null_cons [in Huffman.Code]
not_null_inv [in Huffman.Code]
number_of_nodes_inb_le [in Huffman.BTree]
number_of_occurrences_permutation [in Huffman.Frequency]
number_of_occurrences_app [in Huffman.Frequency]
number_of_occurrences_permutation_ex [in Huffman.Frequency]
number_of_occurrences_O [in Huffman.Frequency]


O

one_cover_ex [in Huffman.Cover]
one_step_comp [in Huffman.OneStep]
one_step_same_sum_leaves [in Huffman.OneStep]
one_step_weight_tree_list [in Huffman.OneStep]
ordered_sum_leaves_eq [in Huffman.WeightTree]
ordered_cover_cover [in Huffman.OrderedCover]
ordered_map_inv [in Huffman.Ordered]
ordered_perm_antisym_eq [in Huffman.Ordered]
ordered_trans_app [in Huffman.Ordered]
ordered_trans [in Huffman.Ordered]
ordered_skip [in Huffman.Ordered]
ordered_inv [in Huffman.Ordered]
ordered_inv_order [in Huffman.Ordered]
ordered_cover_height_pred [in Huffman.HeightPred]
ordered_cover_subst_pred [in Huffman.SubstPred]


P

pbadd_prop2 [in Huffman.PBTree]
pbadd_prop1 [in Huffman.PBTree]
pbbuild_pbnode [in Huffman.PBTree]
pbbuild_true_pbright [in Huffman.PBTree]
pbbuild_compute_peq [in Huffman.PBTree]
pbbuild_distinct_pbleaves [in Huffman.PBTree]
pbbuild_compute_perm [in Huffman.PBTree]
pbfree_pbbuild_prop1 [in Huffman.PBTree]
pbfree_pbadd_prop2 [in Huffman.PBTree]
pbfree_pbadd_prop1 [in Huffman.PBTree]
pbleaf_or_not [in Huffman.PBTree]
pb_unique_prefix [in Huffman.PBTree]
pb_unique_key [in Huffman.PBTree]
pb_unique_prefix1 [in Huffman.PBTree]
permutation_flat_map [in Huffman.Permutation]
permutation_map_ex [in Huffman.Permutation]
permutation_map_ex_aux [in Huffman.Permutation]
permutation_map [in Huffman.Permutation]
permutation_all_permutations [in Huffman.Permutation]
permutation_all_permutations_aux [in Huffman.Permutation]
permutation_inv [in Huffman.Permutation]
permutation_cons_ex [in Huffman.Permutation]
permutation_cons_ex_aux [in Huffman.Permutation]
permutation_transposition [in Huffman.Permutation]
permutation_app_swap [in Huffman.Permutation]
permutation_app_comp [in Huffman.Permutation]
permutation_in [in Huffman.Permutation]
permutation_one_inv [in Huffman.Permutation]
permutation_one_inv_aux [in Huffman.Permutation]
permutation_nil_inv [in Huffman.Permutation]
permutation_length [in Huffman.Permutation]
permutation_sym [in Huffman.Permutation]
permutation_refl [in Huffman.Permutation]
plus_minus_simpl4 [in Huffman.Aux]
prod2list_reorder2 [in Huffman.Prod2List]
prod2list_reorder [in Huffman.Prod2List]
prod2list_eq [in Huffman.Prod2List]
prod2list_le_r [in Huffman.Prod2List]
prod2list_le_l [in Huffman.Prod2List]
prod2list_app [in Huffman.Prod2List]


R

restrict_code_pbbuild [in Huffman.Restrict]
restrict_not_null [in Huffman.Restrict]
restrict_unique_prefix [in Huffman.Restrict]
restrict_code_encode [in Huffman.Restrict]
restrict_code_encode_incl [in Huffman.Restrict]
restrict_code_in [in Huffman.Restrict]
restrict_code_unique_key [in Huffman.Restrict]
restrict_code_encode_length [in Huffman.Weight]
restrict_code_encode_length_inc [in Huffman.Weight]
restrict_code_in [in Huffman.Weight]
restrict_code_unique_key [in Huffman.Weight]


S

same_length_ex [in Huffman.Aux]
same_sum_leaves_length [in Huffman.SameSumLeaves]
skip_n_id [in Huffman.Aux]
skip_n_length [in Huffman.Aux]
skip_n_app2 [in Huffman.Aux]
skip_n_app1 [in Huffman.Aux]
split_one_in_ex [in Huffman.Permutation]
split_one_permutation [in Huffman.Permutation]
subst_pred_length [in Huffman.SubstPred]
subst_pred_ordered_cover_r [in Huffman.SubstPred]
subst_pred_ordered_cover_l [in Huffman.SubstPred]


T

to_btree_smaller [in Huffman.PBTree2BTree]
to_btree_distinct_pbleaves [in Huffman.PBTree2BTree]
to_btree_distinct_leaves [in Huffman.PBTree2BTree]
to_btree_all_leaves [in Huffman.PBTree2BTree]
to_btree_inpb [in Huffman.PBTree2BTree]
to_btree_inb [in Huffman.PBTree2BTree]


U

ulist_unique_key [in Huffman.Weight]
ulist_ordered_cover [in Huffman.OrderedCover]
ulist_pbadd_prop2 [in Huffman.PBTree]
ulist_unique_key [in Huffman.UniqueKey]
ulist_perm [in Huffman.UList]
ulist_app_inv_r [in Huffman.UList]
ulist_app_inv_l [in Huffman.UList]
ulist_app_inv [in Huffman.UList]
ulist_app [in Huffman.UList]
ulist_inv [in Huffman.UList]
unique_key_map [in Huffman.UniqueKey]
unique_key_ulist [in Huffman.UniqueKey]
unique_key_app [in Huffman.UniqueKey]
unique_key_perm [in Huffman.UniqueKey]
unique_key_in_inv [in Huffman.UniqueKey]
unique_key_in [in Huffman.UniqueKey]
unique_key_inv [in Huffman.UniqueKey]
unique_prefix_permutation [in Huffman.Code]
unique_prefix_not_null [in Huffman.Code]
unique_prefix_inv [in Huffman.Code]
unique_prefix2 [in Huffman.Code]
unique_prefix1 [in Huffman.Code]
unique_prefix_nil [in Huffman.Code]


W

weight_tree_list_permutation [in Huffman.WeightTree]
weight_tree_list_node [in Huffman.WeightTree]
weight_permutation [in Huffman.Weight]
weight_tree_compute [in Huffman.HeightPred]



Constructor Index

B

build_step [in Huffman.Build]
build_one [in Huffman.Build]


C

cover_node [in Huffman.Cover]
cover_one [in Huffman.Cover]


H

height_pred_node [in Huffman.HeightPred]
height_pred_nil [in Huffman.HeightPred]


I

inleaf [in Huffman.BTree]
innodeL [in Huffman.BTree]
innodeR [in Huffman.BTree]
inpb_node_r [in Huffman.PBTree]
inpb_node_l [in Huffman.PBTree]
inpb_right [in Huffman.PBTree]
inpb_left [in Huffman.PBTree]
inpb_leaf [in Huffman.PBTree]


L

leaf [in Huffman.BTree]


N

node [in Huffman.BTree]


O

ordered_cover_node [in Huffman.OrderedCover]
ordered_cover_one [in Huffman.OrderedCover]
ordered_cons [in Huffman.Ordered]
ordered_one [in Huffman.Ordered]
ordered_nil [in Huffman.Ordered]


P

pbfree_node2 [in Huffman.PBTree]
pbfree_node1 [in Huffman.PBTree]
pbfree_right2 [in Huffman.PBTree]
pbfree_right1 [in Huffman.PBTree]
pbfree_left2 [in Huffman.PBTree]
pbfree_left1 [in Huffman.PBTree]
pbleaf [in Huffman.PBTree]
pbleft [in Huffman.PBTree]
pbnode [in Huffman.PBTree]
pbright [in Huffman.PBTree]
permutation_trans [in Huffman.Permutation]
permutation_swap [in Huffman.Permutation]
permutation_skip [in Huffman.Permutation]
permutation_nil [in Huffman.Permutation]
prefixCons [in Huffman.Code]
prefixNull [in Huffman.Code]


S

subst_pred_node [in Huffman.SubstPred]
subst_pred_id [in Huffman.SubstPred]


U

ulist_cons [in Huffman.UList]
ulist_nil [in Huffman.UList]
unique_key_cons [in Huffman.UniqueKey]
unique_key_nil [in Huffman.UniqueKey]



Inductive Index

B

btree [in Huffman.BTree]
build [in Huffman.Build]


C

cover [in Huffman.Cover]


H

height_pred [in Huffman.HeightPred]


I

inb [in Huffman.BTree]
inpb [in Huffman.PBTree]
is_prefix [in Huffman.Code]


O

ordered [in Huffman.Ordered]
ordered_cover [in Huffman.OrderedCover]


P

pbfree [in Huffman.PBTree]
pbtree [in Huffman.PBTree]
permutation [in Huffman.Permutation]


S

subst_pred [in Huffman.SubstPred]


U

ulist [in Huffman.UList]
unique_key [in Huffman.UniqueKey]



Section Index

B

Build [in Huffman.Build]


C

Code [in Huffman.Code]
Cover [in Huffman.Cover]
CoverMin [in Huffman.CoverMin]


E

EqBool [in Huffman.Aux]


F

FindMin [in Huffman.Aux]
First [in Huffman.Aux]
FirstMax [in Huffman.Aux]
fold [in Huffman.Aux]
Frequency [in Huffman.Frequency]


H

HeightPred [in Huffman.HeightPred]
Huffman [in Huffman.Huffman]


I

ISortExample [in Huffman.ISort]


L

LeBool [in Huffman.Aux]
List [in Huffman.Aux]


M

map2 [in Huffman.Aux]
Minus [in Huffman.Aux]


O

OneStep [in Huffman.OneStep]
ordered [in Huffman.Ordered]
OrderedCover [in Huffman.OrderedCover]


P

PBTree [in Huffman.PBTree]
PBTREE2BTREE [in Huffman.PBTree2BTree]
permutation [in Huffman.Permutation]
Prod2List [in Huffman.Prod2List]


R

Restrict [in Huffman.Restrict]


S

SameSumLeaves [in Huffman.SameSumLeaves]
SubstPred [in Huffman.SubstPred]


T

Tree [in Huffman.BTree]


U

UniqueKey [in Huffman.UniqueKey]
UniqueList [in Huffman.UList]


W

Weight [in Huffman.Weight]
WeightTree [in Huffman.WeightTree]



Definition Index

A

add_frequency_list [in Huffman.Frequency]
all_permutations [in Huffman.Permutation]
all_permutations_aux [in Huffman.Permutation]
all_cover [in Huffman.Cover]
all_cover_aux [in Huffman.Cover]
all_leaves [in Huffman.BTree]
all_pbleaves [in Huffman.PBTree]


B

btree_dec [in Huffman.BTree]
buildf [in Huffman.Build]
build_fun [in Huffman.Build]


C

code [in Huffman.Code]
code_dec [in Huffman.Code]
compute_code [in Huffman.BTree]
compute_pbcode [in Huffman.PBTree]
cover_dec [in Huffman.Cover]
cover_min [in Huffman.CoverMin]


D

decode [in Huffman.Code]
decode_aux [in Huffman.Code]
distinct_leaves_dec [in Huffman.BTree]
distinct_leaves [in Huffman.BTree]
distinct_pbleaves [in Huffman.PBTree]


E

encode [in Huffman.Code]
eq_bool_dec [in Huffman.Aux]


F

find_max [in Huffman.Aux]
find_min [in Huffman.Aux]
find_val [in Huffman.Code]
find_code [in Huffman.Code]
first_n [in Huffman.Aux]
frequency_list [in Huffman.Frequency]


H

huffman [in Huffman.Huffman]
huffman_aux [in Huffman.Huffman]


I

id_list [in Huffman.Frequency]
inb_dec [in Huffman.BTree]
inpb_dec [in Huffman.PBTree]
insert [in Huffman.ISort]
in_alphabet_dec [in Huffman.Code]
in_alphabet [in Huffman.Code]
isort [in Huffman.ISort]


L

le_sum [in Huffman.WeightTree]
le_bool [in Huffman.Aux]
list_length_induction [in Huffman.Aux]


M

map2 [in Huffman.Aux]


N

not_null [in Huffman.Code]
number_of_nodes [in Huffman.BTree]
number_of_occurrences [in Huffman.Frequency]


O

obuildf [in Huffman.Build]
one_step [in Huffman.OneStep]


P

pbadd [in Huffman.PBTree]
pbbuild [in Huffman.PBTree]
pbtree_dec [in Huffman.PBTree]
permutation_dec [in Huffman.Permutation]
prod2list [in Huffman.Prod2List]


R

restrict_code [in Huffman.Restrict]
restrict_code [in Huffman.Weight]


S

same_sum_leaves [in Huffman.SameSumLeaves]
skip_n [in Huffman.Aux]
split_one [in Huffman.Permutation]
sum_order [in Huffman.WeightTree]
sum_leaves [in Huffman.WeightTree]


T

to_btree [in Huffman.PBTree2BTree]


U

ulist_dec [in Huffman.UList]
unique_prefix [in Huffman.Code]


W

weight [in Huffman.Weight]
weight_tree_list [in Huffman.WeightTree]
weight_tree [in Huffman.WeightTree]



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 (554 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 (74 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 (26 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 (299 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 (43 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 (15 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 (32 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 (65 entries)