| 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 | (537 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 | (72 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 | (25 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 | (287 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 | (31 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 | (64 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.AuxLib]
app_inv_app [lemma, in Huffman.AuxLib]
AuxLib [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]
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]
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]
exist_first_max [lemma, in Huffman.AuxLib]
Extraction [library]
F
FindMin [section, in Huffman.AuxLib]FindMin.A [variable, in Huffman.AuxLib]
FindMin.f [variable, in Huffman.AuxLib]
find_max_correct [lemma, in Huffman.AuxLib]
find_max [definition, in Huffman.AuxLib]
find_min_correct [lemma, in Huffman.AuxLib]
find_min [definition, in Huffman.AuxLib]
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.AuxLib]
FirstMax [section, in Huffman.AuxLib]
firstn_le_length_eq [lemma, in Huffman.AuxLib]
firstn_le_app2 [lemma, in Huffman.AuxLib]
firstn_le_app1 [lemma, in Huffman.AuxLib]
First.A [variable, in Huffman.AuxLib]
Fold [section, in Huffman.AuxLib]
fold_left_init [lemma, in Huffman.AuxLib]
fold_left_map [lemma, in Huffman.AuxLib]
fold_left_eta [lemma, in Huffman.AuxLib]
fold_left_permutation [lemma, in Huffman.Permutation]
fold_plus_permutation [lemma, in Huffman.Weight]
fold_plus_split [lemma, in Huffman.Weight]
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.AuxLib]
Fold.B [variable, in Huffman.AuxLib]
Fold.f [variable, in Huffman.AuxLib]
Fold.g [variable, in Huffman.AuxLib]
Fold.h [variable, in Huffman.AuxLib]
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_subst_pred [lemma, in Huffman.SubstPred]
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]
huffman [definition, in Huffman.Huffman]
Huffman [section, in Huffman.Huffman]
Huffman [library]
huffman_aux [definition, in Huffman.Huffman]
huffman_aux_F [definition, in Huffman.Huffman]
huffman_aux_type [definition, in Huffman.Huffman]
huffman_build_minimum [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_flat_map_ex [lemma, in Huffman.AuxLib]
in_flat_map_in [lemma, in Huffman.AuxLib]
in_map_fst_inv [lemma, in Huffman.AuxLib]
in_map_inv [lemma, in Huffman.AuxLib]
in_ex_app [lemma, in Huffman.AuxLib]
in_permutation_ex [lemma, in Huffman.Permutation]
in_alphabet_compute_code [lemma, in Huffman.BTree]
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]
in_pbleaf_node [lemma, in Huffman.PBTree]
in_pbcompute_inpb [lemma, in Huffman.PBTree]
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.AuxLib]
length_skipn [lemma, in Huffman.AuxLib]
length_compute_lt_O [lemma, in Huffman.BTree]
length_encode_nId [lemma, in Huffman.Weight]
le_bool_correct4 [lemma, in Huffman.AuxLib]
le_bool_correct3 [lemma, in Huffman.AuxLib]
le_bool_correct2 [lemma, in Huffman.AuxLib]
le_bool_correct1 [lemma, in Huffman.AuxLib]
le_bool [definition, in Huffman.AuxLib]
le_minus [lemma, in Huffman.AuxLib]
le_sum_correct2 [lemma, in Huffman.WeightTree]
le_sum_correct1 [lemma, in Huffman.WeightTree]
le_sum [definition, in Huffman.WeightTree]
List [section, in Huffman.AuxLib]
list_length_induction [definition, in Huffman.AuxLib]
list_length_ind [lemma, in Huffman.AuxLib]
List.A [variable, in Huffman.AuxLib]
List.B [variable, in Huffman.AuxLib]
List.C [variable, in Huffman.AuxLib]
List.f [variable, in Huffman.AuxLib]
lt_minus_O [lemma, in Huffman.AuxLib]
M
map2 [definition, in Huffman.AuxLib]map2 [section, in Huffman.AuxLib]
map2_app [lemma, in Huffman.AuxLib]
map2.A [variable, in Huffman.AuxLib]
map2.B [variable, in Huffman.AuxLib]
map2.C [variable, in Huffman.AuxLib]
map2.f [variable, in Huffman.AuxLib]
Minus [section, in Huffman.AuxLib]
minus_minus_simpl4 [lemma, in Huffman.AuxLib]
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_subst_pred [lemma, in Huffman.SubstPred]
ordered_cover_height_pred [lemma, in Huffman.HeightPred]
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.AuxLib]
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.AuxLib]
same_sum_leaves_length [lemma, in Huffman.SameSumLeaves]
same_sum_leaves [definition, in Huffman.SameSumLeaves]
skipn_length_all [lemma, in Huffman.AuxLib]
skipn_le_app2 [lemma, in Huffman.AuxLib]
skipn_le_app1 [lemma, in Huffman.AuxLib]
split_one_in_ex [lemma, in Huffman.Permutation]
split_one_permutation [lemma, in Huffman.Permutation]
split_one [definition, in Huffman.Permutation]
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_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]
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]
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_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]
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]
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]
F
FindMin.A [in Huffman.AuxLib]FindMin.f [in Huffman.AuxLib]
First.A [in Huffman.AuxLib]
Fold.A [in Huffman.AuxLib]
Fold.B [in Huffman.AuxLib]
Fold.f [in Huffman.AuxLib]
Fold.g [in Huffman.AuxLib]
Fold.h [in Huffman.AuxLib]
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.AuxLib]List.B [in Huffman.AuxLib]
List.C [in Huffman.AuxLib]
List.f [in Huffman.AuxLib]
M
map2.A [in Huffman.AuxLib]map2.B [in Huffman.AuxLib]
map2.C [in Huffman.AuxLib]
map2.f [in Huffman.AuxLib]
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
AuxLibB
BTreeBuild
C
CodeCover
CoverMin
E
ExtractionF
FrequencyH
HeightPredHuffman
I
ISortO
OneStepOrdered
OrderedCover
P
PBTreePBTree2BTree
Permutation
Prod2List
R
RestrictS
SameSumLeavesSubstPred
U
UListUniqueKey
W
WeightWeightTree
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.AuxLib]
app_inv_app [in Huffman.AuxLib]
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]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.AuxLib]
F
find_max_correct [in Huffman.AuxLib]find_min_correct [in Huffman.AuxLib]
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]
firstn_le_length_eq [in Huffman.AuxLib]
firstn_le_app2 [in Huffman.AuxLib]
firstn_le_app1 [in Huffman.AuxLib]
fold_left_init [in Huffman.AuxLib]
fold_left_map [in Huffman.AuxLib]
fold_left_eta [in Huffman.AuxLib]
fold_left_permutation [in Huffman.Permutation]
fold_plus_permutation [in Huffman.Weight]
fold_plus_split [in Huffman.Weight]
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_subst_pred [in Huffman.SubstPred]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]
huffman_build_minimum [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_flat_map_ex [in Huffman.AuxLib]
in_flat_map_in [in Huffman.AuxLib]
in_map_fst_inv [in Huffman.AuxLib]
in_map_inv [in Huffman.AuxLib]
in_ex_app [in Huffman.AuxLib]
in_permutation_ex [in Huffman.Permutation]
in_alphabet_compute_code [in Huffman.BTree]
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]
in_pbleaf_node [in Huffman.PBTree]
in_pbcompute_inpb [in Huffman.PBTree]
isort_permutation [in Huffman.ISort]
isort_ordered [in Huffman.ISort]
is_prefix_refl [in Huffman.Code]
L
length_skipn [in Huffman.AuxLib]length_compute_lt_O [in Huffman.BTree]
length_encode_nId [in Huffman.Weight]
le_bool_correct4 [in Huffman.AuxLib]
le_bool_correct3 [in Huffman.AuxLib]
le_bool_correct2 [in Huffman.AuxLib]
le_bool_correct1 [in Huffman.AuxLib]
le_minus [in Huffman.AuxLib]
le_sum_correct2 [in Huffman.WeightTree]
le_sum_correct1 [in Huffman.WeightTree]
list_length_ind [in Huffman.AuxLib]
lt_minus_O [in Huffman.AuxLib]
M
map2_app [in Huffman.AuxLib]minus_minus_simpl4 [in Huffman.AuxLib]
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_subst_pred [in Huffman.SubstPred]
ordered_cover_height_pred [in Huffman.HeightPred]
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.AuxLib]
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.AuxLib]same_sum_leaves_length [in Huffman.SameSumLeaves]
skipn_length_all [in Huffman.AuxLib]
skipn_le_app2 [in Huffman.AuxLib]
skipn_le_app1 [in Huffman.AuxLib]
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_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]
ulist_unique_key [in Huffman.Weight]
ulist_ordered_cover [in Huffman.OrderedCover]
ulist_pbadd_prop2 [in Huffman.PBTree]
ulist_unique_key [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]
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]
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]
F
FindMin [in Huffman.AuxLib]First [in Huffman.AuxLib]
FirstMax [in Huffman.AuxLib]
Fold [in Huffman.AuxLib]
Frequency [in Huffman.Frequency]
H
HeightPred [in Huffman.HeightPred]Huffman [in Huffman.Huffman]
I
ISortExample [in Huffman.ISort]L
LeBool [in Huffman.AuxLib]List [in Huffman.AuxLib]
M
map2 [in Huffman.AuxLib]Minus [in Huffman.AuxLib]
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]F
find_max [in Huffman.AuxLib]find_min [in Huffman.AuxLib]
find_val [in Huffman.Code]
find_code [in Huffman.Code]
frequency_list [in Huffman.Frequency]
H
huffman [in Huffman.Huffman]huffman_aux [in Huffman.Huffman]
huffman_aux_F [in Huffman.Huffman]
huffman_aux_type [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_bool [in Huffman.AuxLib]le_sum [in Huffman.WeightTree]
list_length_induction [in Huffman.AuxLib]
M
map2 [in Huffman.AuxLib]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]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 | (537 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 | (72 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 | (25 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 | (287 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 | (31 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 | (64 entries) |