| 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 | (750 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 | (5 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 | (31 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 | (13 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 | (16 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 | (265 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 | (44 entries) |
| Axiom 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 | (82 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 | (21 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 | (6 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 | (267 entries) |
Global Index
A
Abs [definition, in SearchTree]Abs [definition, in Trie]
abstract [definition, in Trie]
Abs_three_ten [definition, in Trie]
Abs' [definition, in SearchTree]
add_edge [definition, in Color]
adj [definition, in Color]
adj_ext [lemma, in Color]
ADT [library]
ADT_SUMMARY.default [variable, in ADT]
ADT_SUMMARY.V [variable, in ADT]
ADT_SUMMARY [section, in ADT]
B
bag [definition, in BagPerm]BagPerm [library]
bag_eqv_iff_perm [lemma, in BagPerm]
bag_perm [lemma, in BagPerm]
bag_cons_inv [lemma, in BagPerm]
bag_nil_inv [lemma, in BagPerm]
bag_eqv_cons [lemma, in BagPerm]
bag_eqv_trans [lemma, in BagPerm]
bag_eqv_sym [lemma, in BagPerm]
bag_eqv_refl [lemma, in BagPerm]
bag_eqv [definition, in BagPerm]
balance [definition, in Redblack]
balanceP [lemma, in Redblack]
balance_lookup [lemma, in Redblack]
balance_BST [lemma, in Redblack]
balance_BST [lemma, in Redblack]
balance_BST [lemma, in Redblack]
Binom [library]
BinomQueue [module, in Binom]
BinomQueue.Abs [definition, in Binom]
BinomQueue.abs_perm [lemma, in Binom]
BinomQueue.can_relate [lemma, in Binom]
BinomQueue.carry [definition, in Binom]
BinomQueue.carry_elems [lemma, in Binom]
BinomQueue.carry_valid [lemma, in Binom]
BinomQueue.delete_max_Some_relate [lemma, in Binom]
BinomQueue.delete_max_None_relate [lemma, in Binom]
BinomQueue.delete_max_Some_priq [lemma, in Binom]
BinomQueue.delete_max [definition, in Binom]
BinomQueue.delete_max_aux [definition, in Binom]
BinomQueue.empty [definition, in Binom]
BinomQueue.empty_relate [lemma, in Binom]
BinomQueue.empty_priq [lemma, in Binom]
BinomQueue.find_max [definition, in Binom]
BinomQueue.find_max' [definition, in Binom]
BinomQueue.heap_delete_max [definition, in Binom]
BinomQueue.insert [definition, in Binom]
BinomQueue.insert_relate [lemma, in Binom]
BinomQueue.insert_priq [lemma, in Binom]
BinomQueue.join [definition, in Binom]
BinomQueue.join_elems [lemma, in Binom]
BinomQueue.join_valid [lemma, in Binom]
BinomQueue.key [definition, in Binom]
BinomQueue.Leaf [constructor, in Binom]
BinomQueue.manual_grade_for_priqueue_elems [definition, in Binom]
BinomQueue.merge [definition, in Binom]
BinomQueue.merge_relate [lemma, in Binom]
BinomQueue.merge_priq [lemma, in Binom]
BinomQueue.Node [constructor, in Binom]
BinomQueue.pow2heap [definition, in Binom]
BinomQueue.pow2heap' [definition, in Binom]
BinomQueue.priq [definition, in Binom]
BinomQueue.priqueue [definition, in Binom]
BinomQueue.priqueue_elems_ext [lemma, in Binom]
BinomQueue.priqueue_elems [inductive, in Binom]
BinomQueue.priq' [definition, in Binom]
BinomQueue.smash [definition, in Binom]
BinomQueue.smash_elems [lemma, in Binom]
BinomQueue.smash_valid [lemma, in Binom]
BinomQueue.tree [inductive, in Binom]
BinomQueue.tree_can_relate [lemma, in Binom]
BinomQueue.tree_perm [lemma, in Binom]
BinomQueue.tree_elems_ext [lemma, in Binom]
BinomQueue.tree_elems_node [constructor, in Binom]
BinomQueue.tree_elems_leaf [constructor, in Binom]
BinomQueue.tree_elems [inductive, in Binom]
BinomQueue.unzip [definition, in Binom]
Black [constructor, in Redblack]
BST [inductive, in SearchTree]
BST [inductive, in Redblack]
C
cardinal_map [lemma, in Color]color [definition, in Color]
color [inductive, in Redblack]
Color [library]
coloring [definition, in Color]
coloring_ok [definition, in Color]
colors_of [definition, in Color]
color_correct [lemma, in Color]
color1 [definition, in Color]
compute_with_StdLib_lt_dec [lemma, in Decide]
compute_with_lt_dec [lemma, in Decide]
cons_relate [lemma, in ADT]
contents [definition, in Multiset]
contents_perm [lemma, in Multiset]
contents_insert_other [lemma, in Multiset]
contents_cons_inv [lemma, in Multiset]
contents_nil_inv [lemma, in Multiset]
count [definition, in BagPerm]
count_insert_other [lemma, in BagPerm]
create_relate [lemma, in ADT]
D
Decide [library]disjoint [definition, in SearchTree]
domain_example_map [definition, in Color]
E
E [module, in Color]E [constructor, in SearchTree]
E [constructor, in Redblack]
elements [definition, in SearchTree]
elements [definition, in Redblack]
elements_relate' [lemma, in SearchTree]
elements_relate [lemma, in SearchTree]
elements_keys_distinct [lemma, in SearchTree]
elements_empty [lemma, in SearchTree]
elements_slow_elements [lemma, in SearchTree]
elements' [definition, in SearchTree]
elements' [definition, in Redblack]
empty [definition, in Trie]
empty [definition, in Multiset]
empty_relate' [lemma, in SearchTree]
empty_relate [lemma, in SearchTree]
empty_tree_BST [lemma, in SearchTree]
empty_tree [definition, in SearchTree]
empty_relate [lemma, in Trie]
empty_is_trie [lemma, in Trie]
empty_tree_BST [lemma, in Redblack]
empty_tree [definition, in Redblack]
eqb_reflect [lemma, in Perm]
eqlistA_Eeq_eq [lemma, in Color]
equivlistA_example [definition, in Color]
ETABLE [module, in ADT]
ETABLE_INV_MODEL.elements_relate [axiom, in ADT]
ETABLE_INV_MODEL.insert_relate [axiom, in ADT]
ETABLE_INV_MODEL.lookup_relate [axiom, in ADT]
ETABLE_INV_MODEL.empty_relate [axiom, in ADT]
ETABLE_INV_MODEL.Abs [axiom, in ADT]
ETABLE_INV_MODEL.is_table_set [axiom, in ADT]
ETABLE_INV_MODEL.is_table_empty [axiom, in ADT]
ETABLE_INV_MODEL.is_table [axiom, in ADT]
ETABLE_INV_MODEL.elements [axiom, in ADT]
ETABLE_INV_MODEL.set [axiom, in ADT]
ETABLE_INV_MODEL.get [axiom, in ADT]
ETABLE_INV_MODEL.empty [axiom, in ADT]
ETABLE_INV_MODEL.key [definition, in ADT]
ETABLE_INV_MODEL.table [axiom, in ADT]
ETABLE_INV_MODEL.default [axiom, in ADT]
ETABLE_INV_MODEL.V [axiom, in ADT]
ETABLE_INV_MODEL [module, in ADT]
ETABLE_INV.edistinct [axiom, in ADT]
ETABLE_INV.ieg [axiom, in ADT]
ETABLE_INV.gie [axiom, in ADT]
ETABLE_INV.gso [axiom, in ADT]
ETABLE_INV.gss [axiom, in ADT]
ETABLE_INV.gempty [axiom, in ADT]
ETABLE_INV.is_table_set [axiom, in ADT]
ETABLE_INV.is_table_empty [axiom, in ADT]
ETABLE_INV.is_table [axiom, in ADT]
ETABLE_INV.elements [axiom, in ADT]
ETABLE_INV.set [axiom, in ADT]
ETABLE_INV.get [axiom, in ADT]
ETABLE_INV.empty [axiom, in ADT]
ETABLE_INV.key [definition, in ADT]
ETABLE_INV.table [axiom, in ADT]
ETABLE_INV.default [axiom, in ADT]
ETABLE_INV.V [axiom, in ADT]
ETABLE_INV [module, in ADT]
ETABLE.default [axiom, in ADT]
ETABLE.edistinct [axiom, in ADT]
ETABLE.elements [axiom, in ADT]
ETABLE.empty [axiom, in ADT]
ETABLE.gempty [axiom, in ADT]
ETABLE.get [axiom, in ADT]
ETABLE.gie [axiom, in ADT]
ETABLE.gso [axiom, in ADT]
ETABLE.gss [axiom, in ADT]
ETABLE.ieg [axiom, in ADT]
ETABLE.key [definition, in ADT]
ETABLE.set [axiom, in ADT]
ETABLE.table [axiom, in ADT]
ETABLE.V [axiom, in ADT]
even_nat [definition, in ADT]
example_map [definition, in Color]
Experiments [module, in Extract]
Experiments.consecutive [definition, in Extract]
Experiments.E [definition, in Extract]
Experiments.empty_tree [definition, in Extract]
Experiments.insert [definition, in Extract]
Experiments.lookup [definition, in Extract]
Experiments.T [definition, in Extract]
Exploration1 [module, in Perm]
Exploration1.bogus_subtraction [lemma, in Perm]
Exploration1.butterfly [definition, in Perm]
Exploration1.first_le_second [definition, in Perm]
Exploration1.manual_grade_for_Permutation_properties [definition, in Perm]
Exploration1.maybe_swap_correct [lemma, in Perm]
Exploration1.maybe_swap_perm [lemma, in Perm]
Exploration1.maybe_swap_idempotent' [lemma, in Perm]
Exploration1.maybe_swap_idempotent [lemma, in Perm]
Exploration1.maybe_swap_idempotent [lemma, in Perm]
Exploration1.maybe_swap_321 [definition, in Perm]
Exploration1.maybe_swap_123 [definition, in Perm]
Exploration1.maybe_swap [definition, in Perm]
Exploration1.not_a_permutation [definition, in Perm]
Exploration1.omega_example2 [lemma, in Perm]
Exploration1.omega_example1 [lemma, in Perm]
Exploration1.omega_example1 [lemma, in Perm]
Exploration1.permut_example [definition, in Perm]
Extract [library]
F
FastEnough [module, in Trie]FastEnough.collisions [definition, in Trie]
FastEnough.collisions_pi [definition, in Trie]
FastEnough.loop [definition, in Trie]
fib [definition, in ADT]
fibish [definition, in ADT]
fibish_correct [lemma, in ADT]
fibonacci [definition, in ADT]
filter_sortE [lemma, in Color]
find [definition, in SearchTree]
fold_right_rev_left [lemma, in Color]
ForallT [definition, in SearchTree]
ForallT [definition, in Redblack]
ForallT_less [lemma, in Redblack]
ForallT_greater [lemma, in Redblack]
ForallT_imp [lemma, in Redblack]
Forall_app [lemma, in SearchTree]
Forall_perm [lemma, in Perm]
G
G [definition, in Color]graph [definition, in Color]
H
height [definition, in Redblack]I
InA_map_fst_key [lemma, in Color]InA_example [definition, in Color]
ins [definition, in Trie]
ins [definition, in Redblack]
insert [definition, in SearchTree]
insert [definition, in Trie]
insert [definition, in Sort]
insert [definition, in Redblack]
insertion_sort_correct [lemma, in Sort]
insertion_sort_correct [lemma, in BagPerm]
insertion_sort_correct [lemma, in Multiset]
insert_relate' [lemma, in SearchTree]
insert_relate [lemma, in SearchTree]
insert_BST [lemma, in SearchTree]
insert_permute [definition, in SearchTree]
insert_same [definition, in SearchTree]
insert_shadow [definition, in SearchTree]
insert_relate [lemma, in Trie]
insert_is_trie [lemma, in Trie]
insert_sorted' [lemma, in Sort]
insert_sorted [lemma, in Sort]
insert_perm [lemma, in Sort]
insert_bag [lemma, in BagPerm]
insert_is_redblack [lemma, in Redblack]
insert_BST [lemma, in Redblack]
insert_contents [lemma, in Multiset]
insP [lemma, in Redblack]
ins_red [lemma, in Redblack]
ins_is_redblack [lemma, in Redblack]
ins_BST [lemma, in Redblack]
ins_not_E [lemma, in Redblack]
ins_not_E [lemma, in Redblack]
ins_not_E [lemma, in Redblack]
int [axiom, in Extract]
Integers [module, in Trie]
Integers.add [definition, in Trie]
Integers.addc [definition, in Trie]
Integers.addc_correct [lemma, in Trie]
Integers.add_correct [lemma, in Trie]
Integers.compare [definition, in Trie]
Integers.compare_correct [lemma, in Trie]
Integers.comparison [inductive, in Trie]
Integers.Eq [constructor, in Trie]
Integers.Gt [constructor, in Trie]
Integers.Lt [constructor, in Trie]
Integers.positive [inductive, in Trie]
Integers.positive2nat [definition, in Trie]
Integers.positive2nat_pos [lemma, in Trie]
Integers.print_in_binary [definition, in Trie]
Integers.succ [definition, in Trie]
Integers.succ_correct [lemma, in Trie]
Integers.ten [definition, in Trie]
Integers.xH [constructor, in Trie]
Integers.xI [constructor, in Trie]
Integers.xO [constructor, in Trie]
Integers.Z [inductive, in Trie]
Integers.Zneg [constructor, in Trie]
Integers.Zpos [constructor, in Trie]
Integers.Z0 [constructor, in Trie]
_ ~ 0 [notation, in Trie]
_ ~ 1 [notation, in Trie]
int_ltb_reflect [lemma, in Extract]
int2Z [axiom, in Extract]
int2Z_inj [axiom, in Extract]
in_colors_of_1 [lemma, in Color]
in_fst_exists [lemma, in SearchTree]
In_elements_lookup [lemma, in SearchTree]
In_elements_lookup_first_try [lemma, in SearchTree]
in_4_pi [definition, in Decide]
IsRB_b [constructor, in Redblack]
IsRB_r [constructor, in Redblack]
IsRB_leaf [constructor, in Redblack]
is_not_bst [definition, in SearchTree]
is_bst [definition, in SearchTree]
is_trie [definition, in Trie]
is_a_sorting_algorithm [definition, in Selection]
is_a_sorting_algorithm [definition, in Sort]
is_a_sorting_algorithm' [definition, in BagPerm]
is_redblack_toblack [lemma, in Redblack]
is_redblack [inductive, in Redblack]
is_a_sorting_algorithm' [definition, in Multiset]
K
key [definition, in SearchTree]key [definition, in Redblack]
kvs_insert_elements [lemma, in SearchTree]
kvs_insert_split [lemma, in SearchTree]
kvs_insert [definition, in SearchTree]
L
L [module, in ADT]Leaf [constructor, in Trie]
leb_reflect [lemma, in Perm]
LISTISH [module, in ADT]
LISTISH.cons [axiom, in ADT]
LISTISH.create [axiom, in ADT]
LISTISH.list [axiom, in ADT]
LISTISH.nth [axiom, in ADT]
list_ind2 [definition, in Merge]
list_ind2_principle [definition, in Merge]
list_nat_in [definition, in Decide]
list_nat_eq_dec [definition, in Decide]
List_Priqueue.merge_relate [lemma, in Priqueue]
List_Priqueue.merge_priq [lemma, in Priqueue]
List_Priqueue.delete_max_Some_relate [lemma, in Priqueue]
List_Priqueue.delete_max_None_relate [lemma, in Priqueue]
List_Priqueue.delete_max_Some_priq [lemma, in Priqueue]
List_Priqueue.insert_relate [lemma, in Priqueue]
List_Priqueue.insert_priq [lemma, in Priqueue]
List_Priqueue.empty_relate [lemma, in Priqueue]
List_Priqueue.empty_priq [lemma, in Priqueue]
List_Priqueue.abs_perm [lemma, in Priqueue]
List_Priqueue.can_relate [lemma, in Priqueue]
List_Priqueue.Abs [definition, in Priqueue]
List_Priqueue.Abs_intro [constructor, in Priqueue]
List_Priqueue.Abs' [inductive, in Priqueue]
List_Priqueue.priq [definition, in Priqueue]
List_Priqueue.merge [definition, in Priqueue]
List_Priqueue.delete_max [definition, in Priqueue]
List_Priqueue.insert [definition, in Priqueue]
List_Priqueue.empty [definition, in Priqueue]
List_Priqueue.priqueue [definition, in Priqueue]
List_Priqueue.key [definition, in Priqueue]
List_Priqueue.select_biggest [lemma, in Priqueue]
List_Priqueue.select_biggest_aux [lemma, in Priqueue]
List_Priqueue.select_perm [lemma, in Priqueue]
List_Priqueue.select [definition, in Priqueue]
List_Priqueue [module, in Priqueue]
list2map [definition, in SearchTree]
list2map_app [lemma, in SearchTree]
list2map_no [lemma, in SearchTree]
list2map_yes [lemma, in SearchTree]
look [definition, in Trie]
lookup [definition, in SearchTree]
lookup [definition, in Trie]
lookup [definition, in Redblack]
lookup_relate' [lemma, in SearchTree]
lookup_relate [lemma, in SearchTree]
lookup_In_elements [lemma, in SearchTree]
lookup_In_elements_second_try [lemma, in SearchTree]
lookup_In_elements_first_try [lemma, in SearchTree]
lookup_insert_permute [lemma, in SearchTree]
lookup_insert_same [lemma, in SearchTree]
lookup_insert_shadow [lemma, in SearchTree]
lookup_insert_neq' [lemma, in SearchTree]
lookup_insert_neq [lemma, in SearchTree]
lookup_insert_eq' [lemma, in SearchTree]
lookup_insert_eq [lemma, in SearchTree]
lookup_empty [lemma, in SearchTree]
lookup_relate [lemma, in Trie]
lookup_insert_neq [lemma, in Redblack]
lookup_insert_eq [lemma, in Redblack]
lookup_ins_neq [lemma, in Redblack]
lookup_ins_eq [lemma, in Redblack]
lookup_empty [lemma, in Redblack]
look_ins_other [lemma, in Trie]
look_ins_same [lemma, in Trie]
look_leaf [lemma, in Trie]
low_deg [definition, in Color]
ltb [axiom, in Extract]
ltb_reflect [lemma, in Perm]
ltb_lt [axiom, in Extract]
lt_proper [lemma, in Color]
lt_strict [lemma, in Color]
L_Abs [inductive, in ADT]
L.cons [definition, in ADT]
L.create [definition, in ADT]
L.list [definition, in ADT]
L.nth [definition, in ADT]
M
M [module, in Color]makeBlack [definition, in Redblack]
makeblack_fiddle [lemma, in Redblack]
manual_grade_for_elements_spec [definition, in SearchTree]
manual_grade_for_successor_of_Z_constant_time [definition, in Trie]
manual_grade_for_permutations_vs_multiset [definition, in BagPerm]
manual_grade_for_permutations_vs_multiset [definition, in Multiset]
manual_grade_for_TreeTableModel2 [definition, in ADT]
manual_grade_for_TreeTableModel [definition, in ADT]
manual_grade_for_ListsETable [definition, in ADT]
manual_grade_for_ListsTable [definition, in ADT]
MapsTable [module, in ADT]
MapsTable.default [definition, in ADT]
MapsTable.empty [definition, in ADT]
MapsTable.gempty [lemma, in ADT]
MapsTable.get [definition, in ADT]
MapsTable.gso [lemma, in ADT]
MapsTable.gss [lemma, in ADT]
MapsTable.key [definition, in ADT]
MapsTable.set [definition, in ADT]
MapsTable.table [definition, in ADT]
MapsTable.V [definition, in ADT]
Mdomain [definition, in Color]
merge [definition, in Merge]
Merge [library]
mergesort_correct [lemma, in Merge]
mergesort_perm [lemma, in Merge]
mergesort_sorts [lemma, in Merge]
merge_perm [lemma, in Merge]
merge_nil_l [lemma, in Merge]
merge2 [lemma, in Merge]
mindepth [definition, in Redblack]
mk_graph [definition, in Color]
Mremove_cardinal_less [lemma, in Color]
Mremove_elements [lemma, in Color]
multiset [definition, in Multiset]
Multiset [library]
N
nat2pos [definition, in Trie]nat2pos_injective [lemma, in Trie]
nat2pos2nat [lemma, in Trie]
nearly_redblack [inductive, in Redblack]
node [definition, in Color]
Node [constructor, in Trie]
nodemap [definition, in Color]
nodes [definition, in Color]
nodeset [definition, in Color]
NoDup_append [lemma, in SearchTree]
no_selfloop [definition, in Color]
nrRB_b [constructor, in Redblack]
nrRB_r [constructor, in Redblack]
nth_error_insert [lemma, in Sort]
nth_relate [lemma, in ADT]
nth_firstn [lemma, in ADT]
O
out_of_gas [definition, in Selection]O_Abs [definition, in ADT]
P
palette [definition, in Color]Perm [library]
perm_bag [lemma, in BagPerm]
perm_contents [lemma, in Multiset]
pos2nat [definition, in Trie]
pos2nat_injective [lemma, in Trie]
pos2nat2pos [lemma, in Trie]
Preface [library]
PRIQUEUE [module, in Priqueue]
Priqueue [library]
PRIQUEUE.Abs [axiom, in Priqueue]
PRIQUEUE.abs_perm [axiom, in Priqueue]
PRIQUEUE.can_relate [axiom, in Priqueue]
PRIQUEUE.delete_max_Some_relate [axiom, in Priqueue]
PRIQUEUE.delete_max_Some_priq [axiom, in Priqueue]
PRIQUEUE.delete_max_None_relate [axiom, in Priqueue]
PRIQUEUE.delete_max [axiom, in Priqueue]
PRIQUEUE.empty [axiom, in Priqueue]
PRIQUEUE.empty_relate [axiom, in Priqueue]
PRIQUEUE.empty_priq [axiom, in Priqueue]
PRIQUEUE.insert [axiom, in Priqueue]
PRIQUEUE.insert_relate [axiom, in Priqueue]
PRIQUEUE.insert_priq [axiom, in Priqueue]
PRIQUEUE.key [definition, in Priqueue]
PRIQUEUE.merge [axiom, in Priqueue]
PRIQUEUE.merge_relate [axiom, in Priqueue]
PRIQUEUE.merge_priq [axiom, in Priqueue]
PRIQUEUE.priq [axiom, in Priqueue]
PRIQUEUE.priqueue [axiom, in Priqueue]
Proper_eq_key_elt [lemma, in Color]
Proper_eq_eq [lemma, in Color]
R
RatherSlow [module, in Trie]RatherSlow.collisions [definition, in Trie]
RatherSlow.collisions_pi [definition, in Trie]
RatherSlow.empty [definition, in Trie]
RatherSlow.loop [definition, in Trie]
RatherSlow.total_mapz [definition, in Trie]
RatherSlow.update [definition, in Trie]
Red [constructor, in Redblack]
Redblack [library]
redblack_balanced [lemma, in Redblack]
reflect_example2 [definition, in Perm]
reflect_example1' [definition, in Perm]
reflect_example1 [definition, in Perm]
remove_node [definition, in Color]
repeat [definition, in ADT]
repeat_step_relate [lemma, in ADT]
S
S [module, in Color]same_mod_10 [definition, in Color]
same_contents_iff_perm [lemma, in Multiset]
ScratchPad [module, in Decide]
ScratchPad.greater23 [lemma, in Decide]
ScratchPad.is_3_less_7 [definition, in Decide]
ScratchPad.left [constructor, in Decide]
ScratchPad.less37 [lemma, in Decide]
ScratchPad.lt_dec_equivalent [lemma, in Decide]
ScratchPad.lt_dec' [definition, in Decide]
ScratchPad.lt_dec [definition, in Decide]
ScratchPad.right [constructor, in Decide]
ScratchPad.sumbool [inductive, in Decide]
ScratchPad.t1 [definition, in Decide]
ScratchPad.t2 [definition, in Decide]
ScratchPad.t4 [definition, in Decide]
ScratchPad.v1a [definition, in Decide]
ScratchPad.v1b [definition, in Decide]
ScratchPad.v2a [definition, in Decide]
ScratchPad.v3 [definition, in Decide]
{ _ } + { _ } (type_scope) [notation, in Decide]
ScratchPad2 [module, in Decide]
ScratchPad2.insert [definition, in Decide]
ScratchPad2.insert_sorted [lemma, in Decide]
ScratchPad2.le_dec [definition, in Decide]
ScratchPad2.lt_dec_axiom_2 [axiom, in Decide]
ScratchPad2.lt_dec_axiom_1 [axiom, in Decide]
ScratchPad2.lt_dec [definition, in Decide]
ScratchPad2.max_with_axiom [definition, in Decide]
ScratchPad2.prove_with_max_axiom [lemma, in Decide]
ScratchPad2.sort [definition, in Decide]
ScratchPad2.sorted [inductive, in Decide]
ScratchPad2.sorted_cons [constructor, in Decide]
ScratchPad2.sorted_1 [constructor, in Decide]
ScratchPad2.sorted_nil [constructor, in Decide]
SearchTree [library]
SearchTree2 [module, in Extract]
SearchTree2.E [constructor, in Extract]
SearchTree2.elements [definition, in Extract]
SearchTree2.elements' [definition, in Extract]
SearchTree2.empty_tree [definition, in Extract]
SearchTree2.insert [definition, in Extract]
SearchTree2.key [definition, in Extract]
SearchTree2.lookup [definition, in Extract]
SearchTree2.lookup_insert_neq [lemma, in Extract]
SearchTree2.lookup_insert_eq [lemma, in Extract]
SearchTree2.lookup_empty [lemma, in Extract]
SearchTree2.T [constructor, in Extract]
SearchTree2.tree [inductive, in Extract]
SearchTree2.TREES [section, in Extract]
SearchTree2.TREES.default [variable, in Extract]
SearchTree2.TREES.V [variable, in Extract]
SectionExample1 [module, in SearchTree]
SectionExample1.empty [definition, in SearchTree]
SectionExample1.lookup [definition, in SearchTree]
SectionExample1.lookup_empty [lemma, in SearchTree]
SectionExample1.mymap [definition, in SearchTree]
SectionExample2 [module, in SearchTree]
SectionExample2.empty [definition, in SearchTree]
SectionExample2.LISTS [section, in SearchTree]
SectionExample2.LISTS.default [variable, in SearchTree]
SectionExample2.LISTS.V [variable, in SearchTree]
SectionExample2.lookup [definition, in SearchTree]
SectionExample2.lookup_empty [lemma, in SearchTree]
SectionExample2.mymap [definition, in SearchTree]
select [definition, in Selection]
Selection [library]
selection_sort_is_correct [lemma, in Selection]
selection_sort_sorted [lemma, in Selection]
selection_sort_sorted_aux [lemma, in Selection]
selection_sort_perm [lemma, in Selection]
selection_sort_correct [definition, in Selection]
selection_sort [definition, in Selection]
select_terminates [lemma, in Color]
select_smallest [lemma, in Selection]
select_smallest_aux [lemma, in Selection]
select_perm [lemma, in Selection]
select_perm' [lemma, in Selection]
selsort [definition, in Selection]
selsort [definition, in Selection]
selsort_perm [lemma, in Selection]
selsort'_perm [lemma, in Selection]
singleton [definition, in Multiset]
Sin_domain [lemma, in Color]
sixlist [definition, in ADT]
slow_elements_prop [lemma, in SearchTree]
slow_elements [definition, in SearchTree]
Snot_in_empty [lemma, in Color]
sort [definition, in Sort]
Sort [library]
sorted [inductive, in Selection]
sorted [inductive, in Sort]
Sorted_lt_key [lemma, in Color]
sorted_cons [constructor, in Selection]
sorted_1 [constructor, in Selection]
sorted_nil [constructor, in Selection]
sorted_sorted' [lemma, in Sort]
sorted_cons [constructor, in Sort]
sorted_1 [constructor, in Sort]
sorted_nil [constructor, in Sort]
sorted_merge [lemma, in Merge]
sorted_merge1 [lemma, in Merge]
sorted' [definition, in Sort]
sorted'_sorted [lemma, in Sort]
sorted'' [definition, in Sort]
SortE_equivlistE_eqlistE [lemma, in Color]
sort_pi [definition, in Selection]
sort_sorted' [lemma, in Sort]
sort_sorted [lemma, in Sort]
sort_perm [lemma, in Sort]
sort_pi [definition, in Sort]
sort_specifications_equivalent [lemma, in BagPerm]
sort_bag [lemma, in BagPerm]
sort_specifications_equivalent [lemma, in Multiset]
sort_contents [lemma, in Multiset]
sort_pi_same_contents [definition, in Multiset]
sort_pi [definition, in Multiset]
Sort1 [module, in Extract]
Sort1.insert [definition, in Extract]
Sort1.sort [definition, in Extract]
specialize_SortA_equivlistA_eqlistA [lemma, in Color]
split [definition, in Merge]
split_perm [lemma, in Merge]
split_len [lemma, in Merge]
split_len' [lemma, in Merge]
split_len_first_try [lemma, in Merge]
Sremove_cardinal_less [lemma, in Color]
Sremove_elements [lemma, in Color]
Sremove_elements [lemma, in Color]
step [definition, in ADT]
stepish [definition, in ADT]
step_relate [lemma, in ADT]
ST_T [constructor, in SearchTree]
ST_E [constructor, in SearchTree]
ST_T [constructor, in Redblack]
ST_E [constructor, in Redblack]
subset_nodes_sub [lemma, in Color]
subset_nodes [definition, in Color]
T
T [constructor, in SearchTree]T [constructor, in Redblack]
TABLE [module, in ADT]
TABLE.default [axiom, in ADT]
TABLE.empty [axiom, in ADT]
TABLE.gempty [axiom, in ADT]
TABLE.get [axiom, in ADT]
TABLE.gso [axiom, in ADT]
TABLE.gss [axiom, in ADT]
TABLE.key [definition, in ADT]
TABLE.set [axiom, in ADT]
TABLE.table [axiom, in ADT]
TABLE.V [axiom, in ADT]
three_ten [definition, in Trie]
three_less_seven_2 [lemma, in Decide]
three_less_seven_1 [lemma, in Decide]
too_much_gas [definition, in Selection]
tree [inductive, in SearchTree]
tree [inductive, in Redblack]
TreeETable [module, in ADT]
TreeETable.default [definition, in ADT]
TreeETable.edistinct [lemma, in ADT]
TreeETable.elements [definition, in ADT]
TreeETable.empty [definition, in ADT]
TreeETable.gempty [lemma, in ADT]
TreeETable.get [definition, in ADT]
TreeETable.gie [lemma, in ADT]
TreeETable.gso [lemma, in ADT]
TreeETable.gss [lemma, in ADT]
TreeETable.ieg [lemma, in ADT]
TreeETable.key [definition, in ADT]
TreeETable.set [definition, in ADT]
TreeETable.table [definition, in ADT]
TreeETable.V [definition, in ADT]
TreeETable2 [module, in ADT]
TreeETable2.default [definition, in ADT]
TreeETable2.edistinct [lemma, in ADT]
TreeETable2.elements [definition, in ADT]
TreeETable2.empty [definition, in ADT]
TreeETable2.gempty [lemma, in ADT]
TreeETable2.get [definition, in ADT]
TreeETable2.gie [lemma, in ADT]
TreeETable2.gso [lemma, in ADT]
TreeETable2.gss [lemma, in ADT]
TreeETable2.ieg [lemma, in ADT]
TreeETable2.key [definition, in ADT]
TreeETable2.set [definition, in ADT]
TreeETable2.table [definition, in ADT]
TreeETable2.V [definition, in ADT]
TreeETable3 [module, in ADT]
TreeETable3.default [definition, in ADT]
TreeETable3.edistinct [lemma, in ADT]
TreeETable3.elements [definition, in ADT]
TreeETable3.empty [definition, in ADT]
TreeETable3.gempty [lemma, in ADT]
TreeETable3.get [definition, in ADT]
TreeETable3.gie [lemma, in ADT]
TreeETable3.gso [lemma, in ADT]
TreeETable3.gss [lemma, in ADT]
TreeETable3.ieg [lemma, in ADT]
TreeETable3.is_table_set [lemma, in ADT]
TreeETable3.is_table_empty [lemma, in ADT]
TreeETable3.is_table [definition, in ADT]
TreeETable3.key [definition, in ADT]
TreeETable3.set [definition, in ADT]
TreeETable3.table [definition, in ADT]
TreeETable3.V [definition, in ADT]
TREES [section, in SearchTree]
TREES [section, in Redblack]
TREES.default [variable, in Redblack]
TREES.EXAMPLES [section, in SearchTree]
TREES.EXAMPLES.default [variable, in SearchTree]
TREES.EXAMPLES.v2 [variable, in SearchTree]
TREES.EXAMPLES.v4 [variable, in SearchTree]
TREES.EXAMPLES.v5 [variable, in SearchTree]
TREES.V [variable, in SearchTree]
TREES.V [variable, in Redblack]
TreeTable [module, in ADT]
TreeTable.default [definition, in ADT]
TreeTable.elements [definition, in ADT]
TreeTable.empty [definition, in ADT]
TreeTable.gempty [lemma, in ADT]
TreeTable.get [definition, in ADT]
TreeTable.gso [lemma, in ADT]
TreeTable.gss [lemma, in ADT]
TreeTable.key [definition, in ADT]
TreeTable.set [definition, in ADT]
TreeTable.table [definition, in ADT]
TreeTable.V [definition, in ADT]
tree2map [definition, in SearchTree]
tree2map_prop [lemma, in SearchTree]
trie [inductive, in Trie]
Trie [library]
trie_table [definition, in Trie]
T_neq_E [lemma, in Redblack]
U
undirected [definition, in Color]union [definition, in SearchTree]
union [definition, in Multiset]
union_update_left [lemma, in SearchTree]
union_update_right [lemma, in SearchTree]
union_both [lemma, in SearchTree]
union_right [lemma, in SearchTree]
union_left [lemma, in SearchTree]
union_comm [lemma, in Multiset]
union_assoc [lemma, in Multiset]
V
value [definition, in Multiset]VerySlow [module, in Trie]
VerySlow.collisions [definition, in Trie]
VerySlow.collisions_pi [definition, in Trie]
VerySlow.loop [definition, in Trie]
W
WF [module, in Color]WP [module, in Color]
Z
Z_ltb_reflect [lemma, in Extract]Z_eqb_reflect [lemma, in Extract]
other
_ >? _ (nat_scope) [notation, in Perm]_ >=? _ (nat_scope) [notation, in Perm]
Notation Index
I
_ ~ 0 [in Trie]_ ~ 1 [in Trie]
S
{ _ } + { _ } (type_scope) [in Decide]other
_ >? _ (nat_scope) [in Perm]_ >=? _ (nat_scope) [in Perm]
Module Index
B
BinomQueue [in Binom]E
E [in Color]ETABLE [in ADT]
ETABLE_INV_MODEL [in ADT]
ETABLE_INV [in ADT]
Experiments [in Extract]
Exploration1 [in Perm]
F
FastEnough [in Trie]I
Integers [in Trie]L
L [in ADT]LISTISH [in ADT]
List_Priqueue [in Priqueue]
M
M [in Color]MapsTable [in ADT]
P
PRIQUEUE [in Priqueue]R
RatherSlow [in Trie]S
S [in Color]ScratchPad [in Decide]
ScratchPad2 [in Decide]
SearchTree2 [in Extract]
SectionExample1 [in SearchTree]
SectionExample2 [in SearchTree]
Sort1 [in Extract]
T
TABLE [in ADT]TreeETable [in ADT]
TreeETable2 [in ADT]
TreeETable3 [in ADT]
TreeTable [in ADT]
V
VerySlow [in Trie]W
WF [in Color]WP [in Color]
Variable Index
A
ADT_SUMMARY.default [in ADT]ADT_SUMMARY.V [in ADT]
S
SearchTree2.TREES.default [in Extract]SearchTree2.TREES.V [in Extract]
SectionExample2.LISTS.default [in SearchTree]
SectionExample2.LISTS.V [in SearchTree]
T
TREES.default [in Redblack]TREES.EXAMPLES.default [in SearchTree]
TREES.EXAMPLES.v2 [in SearchTree]
TREES.EXAMPLES.v4 [in SearchTree]
TREES.EXAMPLES.v5 [in SearchTree]
TREES.V [in SearchTree]
TREES.V [in Redblack]
Library Index
A
ADTB
BagPermBinom
C
ColorD
DecideE
ExtractM
MergeMultiset
P
PermPreface
Priqueue
R
RedblackS
SearchTreeSelection
Sort
T
TrieLemma Index
A
adj_ext [in Color]B
bag_eqv_iff_perm [in BagPerm]bag_perm [in BagPerm]
bag_cons_inv [in BagPerm]
bag_nil_inv [in BagPerm]
bag_eqv_cons [in BagPerm]
bag_eqv_trans [in BagPerm]
bag_eqv_sym [in BagPerm]
bag_eqv_refl [in BagPerm]
balanceP [in Redblack]
balance_lookup [in Redblack]
balance_BST [in Redblack]
balance_BST [in Redblack]
balance_BST [in Redblack]
BinomQueue.abs_perm [in Binom]
BinomQueue.can_relate [in Binom]
BinomQueue.carry_elems [in Binom]
BinomQueue.carry_valid [in Binom]
BinomQueue.delete_max_Some_relate [in Binom]
BinomQueue.delete_max_None_relate [in Binom]
BinomQueue.delete_max_Some_priq [in Binom]
BinomQueue.empty_relate [in Binom]
BinomQueue.empty_priq [in Binom]
BinomQueue.insert_relate [in Binom]
BinomQueue.insert_priq [in Binom]
BinomQueue.join_elems [in Binom]
BinomQueue.join_valid [in Binom]
BinomQueue.merge_relate [in Binom]
BinomQueue.merge_priq [in Binom]
BinomQueue.priqueue_elems_ext [in Binom]
BinomQueue.smash_elems [in Binom]
BinomQueue.smash_valid [in Binom]
BinomQueue.tree_can_relate [in Binom]
BinomQueue.tree_perm [in Binom]
BinomQueue.tree_elems_ext [in Binom]
C
cardinal_map [in Color]color_correct [in Color]
compute_with_StdLib_lt_dec [in Decide]
compute_with_lt_dec [in Decide]
cons_relate [in ADT]
contents_perm [in Multiset]
contents_insert_other [in Multiset]
contents_cons_inv [in Multiset]
contents_nil_inv [in Multiset]
count_insert_other [in BagPerm]
create_relate [in ADT]
E
elements_relate' [in SearchTree]elements_relate [in SearchTree]
elements_keys_distinct [in SearchTree]
elements_empty [in SearchTree]
elements_slow_elements [in SearchTree]
empty_relate' [in SearchTree]
empty_relate [in SearchTree]
empty_tree_BST [in SearchTree]
empty_relate [in Trie]
empty_is_trie [in Trie]
empty_tree_BST [in Redblack]
eqb_reflect [in Perm]
eqlistA_Eeq_eq [in Color]
Exploration1.bogus_subtraction [in Perm]
Exploration1.maybe_swap_correct [in Perm]
Exploration1.maybe_swap_perm [in Perm]
Exploration1.maybe_swap_idempotent' [in Perm]
Exploration1.maybe_swap_idempotent [in Perm]
Exploration1.maybe_swap_idempotent [in Perm]
Exploration1.omega_example2 [in Perm]
Exploration1.omega_example1 [in Perm]
Exploration1.omega_example1 [in Perm]
F
fibish_correct [in ADT]filter_sortE [in Color]
fold_right_rev_left [in Color]
ForallT_less [in Redblack]
ForallT_greater [in Redblack]
ForallT_imp [in Redblack]
Forall_app [in SearchTree]
Forall_perm [in Perm]
I
InA_map_fst_key [in Color]insertion_sort_correct [in Sort]
insertion_sort_correct [in BagPerm]
insertion_sort_correct [in Multiset]
insert_relate' [in SearchTree]
insert_relate [in SearchTree]
insert_BST [in SearchTree]
insert_relate [in Trie]
insert_is_trie [in Trie]
insert_sorted' [in Sort]
insert_sorted [in Sort]
insert_perm [in Sort]
insert_bag [in BagPerm]
insert_is_redblack [in Redblack]
insert_BST [in Redblack]
insert_contents [in Multiset]
insP [in Redblack]
ins_red [in Redblack]
ins_is_redblack [in Redblack]
ins_BST [in Redblack]
ins_not_E [in Redblack]
ins_not_E [in Redblack]
ins_not_E [in Redblack]
Integers.addc_correct [in Trie]
Integers.add_correct [in Trie]
Integers.compare_correct [in Trie]
Integers.positive2nat_pos [in Trie]
Integers.succ_correct [in Trie]
int_ltb_reflect [in Extract]
in_colors_of_1 [in Color]
in_fst_exists [in SearchTree]
In_elements_lookup [in SearchTree]
In_elements_lookup_first_try [in SearchTree]
is_redblack_toblack [in Redblack]
K
kvs_insert_elements [in SearchTree]kvs_insert_split [in SearchTree]
L
leb_reflect [in Perm]List_Priqueue.merge_relate [in Priqueue]
List_Priqueue.merge_priq [in Priqueue]
List_Priqueue.delete_max_Some_relate [in Priqueue]
List_Priqueue.delete_max_None_relate [in Priqueue]
List_Priqueue.delete_max_Some_priq [in Priqueue]
List_Priqueue.insert_relate [in Priqueue]
List_Priqueue.insert_priq [in Priqueue]
List_Priqueue.empty_relate [in Priqueue]
List_Priqueue.empty_priq [in Priqueue]
List_Priqueue.abs_perm [in Priqueue]
List_Priqueue.can_relate [in Priqueue]
List_Priqueue.select_biggest [in Priqueue]
List_Priqueue.select_biggest_aux [in Priqueue]
List_Priqueue.select_perm [in Priqueue]
list2map_app [in SearchTree]
list2map_no [in SearchTree]
list2map_yes [in SearchTree]
lookup_relate' [in SearchTree]
lookup_relate [in SearchTree]
lookup_In_elements [in SearchTree]
lookup_In_elements_second_try [in SearchTree]
lookup_In_elements_first_try [in SearchTree]
lookup_insert_permute [in SearchTree]
lookup_insert_same [in SearchTree]
lookup_insert_shadow [in SearchTree]
lookup_insert_neq' [in SearchTree]
lookup_insert_neq [in SearchTree]
lookup_insert_eq' [in SearchTree]
lookup_insert_eq [in SearchTree]
lookup_empty [in SearchTree]
lookup_relate [in Trie]
lookup_insert_neq [in Redblack]
lookup_insert_eq [in Redblack]
lookup_ins_neq [in Redblack]
lookup_ins_eq [in Redblack]
lookup_empty [in Redblack]
look_ins_other [in Trie]
look_ins_same [in Trie]
look_leaf [in Trie]
ltb_reflect [in Perm]
lt_proper [in Color]
lt_strict [in Color]
M
makeblack_fiddle [in Redblack]MapsTable.gempty [in ADT]
MapsTable.gso [in ADT]
MapsTable.gss [in ADT]
mergesort_correct [in Merge]
mergesort_perm [in Merge]
mergesort_sorts [in Merge]
merge_perm [in Merge]
merge_nil_l [in Merge]
merge2 [in Merge]
Mremove_cardinal_less [in Color]
Mremove_elements [in Color]
N
nat2pos_injective [in Trie]nat2pos2nat [in Trie]
NoDup_append [in SearchTree]
nth_error_insert [in Sort]
nth_relate [in ADT]
nth_firstn [in ADT]
P
perm_bag [in BagPerm]perm_contents [in Multiset]
pos2nat_injective [in Trie]
pos2nat2pos [in Trie]
Proper_eq_key_elt [in Color]
Proper_eq_eq [in Color]
R
redblack_balanced [in Redblack]repeat_step_relate [in ADT]
S
same_contents_iff_perm [in Multiset]ScratchPad.greater23 [in Decide]
ScratchPad.less37 [in Decide]
ScratchPad.lt_dec_equivalent [in Decide]
ScratchPad2.insert_sorted [in Decide]
ScratchPad2.prove_with_max_axiom [in Decide]
SearchTree2.lookup_insert_neq [in Extract]
SearchTree2.lookup_insert_eq [in Extract]
SearchTree2.lookup_empty [in Extract]
SectionExample1.lookup_empty [in SearchTree]
SectionExample2.lookup_empty [in SearchTree]
selection_sort_is_correct [in Selection]
selection_sort_sorted [in Selection]
selection_sort_sorted_aux [in Selection]
selection_sort_perm [in Selection]
select_terminates [in Color]
select_smallest [in Selection]
select_smallest_aux [in Selection]
select_perm [in Selection]
select_perm' [in Selection]
selsort_perm [in Selection]
selsort'_perm [in Selection]
Sin_domain [in Color]
slow_elements_prop [in SearchTree]
Snot_in_empty [in Color]
Sorted_lt_key [in Color]
sorted_sorted' [in Sort]
sorted_merge [in Merge]
sorted_merge1 [in Merge]
sorted'_sorted [in Sort]
SortE_equivlistE_eqlistE [in Color]
sort_sorted' [in Sort]
sort_sorted [in Sort]
sort_perm [in Sort]
sort_specifications_equivalent [in BagPerm]
sort_bag [in BagPerm]
sort_specifications_equivalent [in Multiset]
sort_contents [in Multiset]
specialize_SortA_equivlistA_eqlistA [in Color]
split_perm [in Merge]
split_len [in Merge]
split_len' [in Merge]
split_len_first_try [in Merge]
Sremove_cardinal_less [in Color]
Sremove_elements [in Color]
Sremove_elements [in Color]
step_relate [in ADT]
subset_nodes_sub [in Color]
T
three_less_seven_2 [in Decide]three_less_seven_1 [in Decide]
TreeETable.edistinct [in ADT]
TreeETable.gempty [in ADT]
TreeETable.gie [in ADT]
TreeETable.gso [in ADT]
TreeETable.gss [in ADT]
TreeETable.ieg [in ADT]
TreeETable2.edistinct [in ADT]
TreeETable2.gempty [in ADT]
TreeETable2.gie [in ADT]
TreeETable2.gso [in ADT]
TreeETable2.gss [in ADT]
TreeETable2.ieg [in ADT]
TreeETable3.edistinct [in ADT]
TreeETable3.gempty [in ADT]
TreeETable3.gie [in ADT]
TreeETable3.gso [in ADT]
TreeETable3.gss [in ADT]
TreeETable3.ieg [in ADT]
TreeETable3.is_table_set [in ADT]
TreeETable3.is_table_empty [in ADT]
TreeTable.gempty [in ADT]
TreeTable.gso [in ADT]
TreeTable.gss [in ADT]
tree2map_prop [in SearchTree]
T_neq_E [in Redblack]
U
union_update_left [in SearchTree]union_update_right [in SearchTree]
union_both [in SearchTree]
union_right [in SearchTree]
union_left [in SearchTree]
union_comm [in Multiset]
union_assoc [in Multiset]
Z
Z_ltb_reflect [in Extract]Z_eqb_reflect [in Extract]
Constructor Index
B
BinomQueue.Leaf [in Binom]BinomQueue.Node [in Binom]
BinomQueue.tree_elems_node [in Binom]
BinomQueue.tree_elems_leaf [in Binom]
Black [in Redblack]
E
E [in SearchTree]E [in Redblack]
I
Integers.Eq [in Trie]Integers.Gt [in Trie]
Integers.Lt [in Trie]
Integers.xH [in Trie]
Integers.xI [in Trie]
Integers.xO [in Trie]
Integers.Zneg [in Trie]
Integers.Zpos [in Trie]
Integers.Z0 [in Trie]
IsRB_b [in Redblack]
IsRB_r [in Redblack]
IsRB_leaf [in Redblack]
L
Leaf [in Trie]List_Priqueue.Abs_intro [in Priqueue]
N
Node [in Trie]nrRB_b [in Redblack]
nrRB_r [in Redblack]
R
Red [in Redblack]S
ScratchPad.left [in Decide]ScratchPad.right [in Decide]
ScratchPad2.sorted_cons [in Decide]
ScratchPad2.sorted_1 [in Decide]
ScratchPad2.sorted_nil [in Decide]
SearchTree2.E [in Extract]
SearchTree2.T [in Extract]
sorted_cons [in Selection]
sorted_1 [in Selection]
sorted_nil [in Selection]
sorted_cons [in Sort]
sorted_1 [in Sort]
sorted_nil [in Sort]
ST_T [in SearchTree]
ST_E [in SearchTree]
ST_T [in Redblack]
ST_E [in Redblack]
T
T [in SearchTree]T [in Redblack]
Axiom Index
E
ETABLE_INV_MODEL.elements_relate [in ADT]ETABLE_INV_MODEL.insert_relate [in ADT]
ETABLE_INV_MODEL.lookup_relate [in ADT]
ETABLE_INV_MODEL.empty_relate [in ADT]
ETABLE_INV_MODEL.Abs [in ADT]
ETABLE_INV_MODEL.is_table_set [in ADT]
ETABLE_INV_MODEL.is_table_empty [in ADT]
ETABLE_INV_MODEL.is_table [in ADT]
ETABLE_INV_MODEL.elements [in ADT]
ETABLE_INV_MODEL.set [in ADT]
ETABLE_INV_MODEL.get [in ADT]
ETABLE_INV_MODEL.empty [in ADT]
ETABLE_INV_MODEL.table [in ADT]
ETABLE_INV_MODEL.default [in ADT]
ETABLE_INV_MODEL.V [in ADT]
ETABLE_INV.edistinct [in ADT]
ETABLE_INV.ieg [in ADT]
ETABLE_INV.gie [in ADT]
ETABLE_INV.gso [in ADT]
ETABLE_INV.gss [in ADT]
ETABLE_INV.gempty [in ADT]
ETABLE_INV.is_table_set [in ADT]
ETABLE_INV.is_table_empty [in ADT]
ETABLE_INV.is_table [in ADT]
ETABLE_INV.elements [in ADT]
ETABLE_INV.set [in ADT]
ETABLE_INV.get [in ADT]
ETABLE_INV.empty [in ADT]
ETABLE_INV.table [in ADT]
ETABLE_INV.default [in ADT]
ETABLE_INV.V [in ADT]
ETABLE.default [in ADT]
ETABLE.edistinct [in ADT]
ETABLE.elements [in ADT]
ETABLE.empty [in ADT]
ETABLE.gempty [in ADT]
ETABLE.get [in ADT]
ETABLE.gie [in ADT]
ETABLE.gso [in ADT]
ETABLE.gss [in ADT]
ETABLE.ieg [in ADT]
ETABLE.set [in ADT]
ETABLE.table [in ADT]
ETABLE.V [in ADT]
I
int [in Extract]int2Z [in Extract]
int2Z_inj [in Extract]
L
LISTISH.cons [in ADT]LISTISH.create [in ADT]
LISTISH.list [in ADT]
LISTISH.nth [in ADT]
ltb [in Extract]
ltb_lt [in Extract]
P
PRIQUEUE.Abs [in Priqueue]PRIQUEUE.abs_perm [in Priqueue]
PRIQUEUE.can_relate [in Priqueue]
PRIQUEUE.delete_max_Some_relate [in Priqueue]
PRIQUEUE.delete_max_Some_priq [in Priqueue]
PRIQUEUE.delete_max_None_relate [in Priqueue]
PRIQUEUE.delete_max [in Priqueue]
PRIQUEUE.empty [in Priqueue]
PRIQUEUE.empty_relate [in Priqueue]
PRIQUEUE.empty_priq [in Priqueue]
PRIQUEUE.insert [in Priqueue]
PRIQUEUE.insert_relate [in Priqueue]
PRIQUEUE.insert_priq [in Priqueue]
PRIQUEUE.merge [in Priqueue]
PRIQUEUE.merge_relate [in Priqueue]
PRIQUEUE.merge_priq [in Priqueue]
PRIQUEUE.priq [in Priqueue]
PRIQUEUE.priqueue [in Priqueue]
S
ScratchPad2.lt_dec_axiom_2 [in Decide]ScratchPad2.lt_dec_axiom_1 [in Decide]
T
TABLE.default [in ADT]TABLE.empty [in ADT]
TABLE.gempty [in ADT]
TABLE.get [in ADT]
TABLE.gso [in ADT]
TABLE.gss [in ADT]
TABLE.set [in ADT]
TABLE.table [in ADT]
TABLE.V [in ADT]
Inductive Index
B
BinomQueue.priqueue_elems [in Binom]BinomQueue.tree [in Binom]
BinomQueue.tree_elems [in Binom]
BST [in SearchTree]
BST [in Redblack]
C
color [in Redblack]I
Integers.comparison [in Trie]Integers.positive [in Trie]
Integers.Z [in Trie]
is_redblack [in Redblack]
L
List_Priqueue.Abs' [in Priqueue]L_Abs [in ADT]
N
nearly_redblack [in Redblack]S
ScratchPad.sumbool [in Decide]ScratchPad2.sorted [in Decide]
SearchTree2.tree [in Extract]
sorted [in Selection]
sorted [in Sort]
T
tree [in SearchTree]tree [in Redblack]
trie [in Trie]
Section Index
A
ADT_SUMMARY [in ADT]S
SearchTree2.TREES [in Extract]SectionExample2.LISTS [in SearchTree]
T
TREES [in SearchTree]TREES [in Redblack]
TREES.EXAMPLES [in SearchTree]
Definition Index
A
Abs [in SearchTree]Abs [in Trie]
abstract [in Trie]
Abs_three_ten [in Trie]
Abs' [in SearchTree]
add_edge [in Color]
adj [in Color]
B
bag [in BagPerm]bag_eqv [in BagPerm]
balance [in Redblack]
BinomQueue.Abs [in Binom]
BinomQueue.carry [in Binom]
BinomQueue.delete_max [in Binom]
BinomQueue.delete_max_aux [in Binom]
BinomQueue.empty [in Binom]
BinomQueue.find_max [in Binom]
BinomQueue.find_max' [in Binom]
BinomQueue.heap_delete_max [in Binom]
BinomQueue.insert [in Binom]
BinomQueue.join [in Binom]
BinomQueue.key [in Binom]
BinomQueue.manual_grade_for_priqueue_elems [in Binom]
BinomQueue.merge [in Binom]
BinomQueue.pow2heap [in Binom]
BinomQueue.pow2heap' [in Binom]
BinomQueue.priq [in Binom]
BinomQueue.priqueue [in Binom]
BinomQueue.priq' [in Binom]
BinomQueue.smash [in Binom]
BinomQueue.unzip [in Binom]
C
color [in Color]coloring [in Color]
coloring_ok [in Color]
colors_of [in Color]
color1 [in Color]
contents [in Multiset]
count [in BagPerm]
D
disjoint [in SearchTree]domain_example_map [in Color]
E
elements [in SearchTree]elements [in Redblack]
elements' [in SearchTree]
elements' [in Redblack]
empty [in Trie]
empty [in Multiset]
empty_tree [in SearchTree]
empty_tree [in Redblack]
equivlistA_example [in Color]
ETABLE_INV_MODEL.key [in ADT]
ETABLE_INV.key [in ADT]
ETABLE.key [in ADT]
even_nat [in ADT]
example_map [in Color]
Experiments.consecutive [in Extract]
Experiments.E [in Extract]
Experiments.empty_tree [in Extract]
Experiments.insert [in Extract]
Experiments.lookup [in Extract]
Experiments.T [in Extract]
Exploration1.butterfly [in Perm]
Exploration1.first_le_second [in Perm]
Exploration1.manual_grade_for_Permutation_properties [in Perm]
Exploration1.maybe_swap_321 [in Perm]
Exploration1.maybe_swap_123 [in Perm]
Exploration1.maybe_swap [in Perm]
Exploration1.not_a_permutation [in Perm]
Exploration1.permut_example [in Perm]
F
FastEnough.collisions [in Trie]FastEnough.collisions_pi [in Trie]
FastEnough.loop [in Trie]
fib [in ADT]
fibish [in ADT]
fibonacci [in ADT]
find [in SearchTree]
ForallT [in SearchTree]
ForallT [in Redblack]
G
G [in Color]graph [in Color]
H
height [in Redblack]I
InA_example [in Color]ins [in Trie]
ins [in Redblack]
insert [in SearchTree]
insert [in Trie]
insert [in Sort]
insert [in Redblack]
insert_permute [in SearchTree]
insert_same [in SearchTree]
insert_shadow [in SearchTree]
Integers.add [in Trie]
Integers.addc [in Trie]
Integers.compare [in Trie]
Integers.positive2nat [in Trie]
Integers.print_in_binary [in Trie]
Integers.succ [in Trie]
Integers.ten [in Trie]
in_4_pi [in Decide]
is_not_bst [in SearchTree]
is_bst [in SearchTree]
is_trie [in Trie]
is_a_sorting_algorithm [in Selection]
is_a_sorting_algorithm [in Sort]
is_a_sorting_algorithm' [in BagPerm]
is_a_sorting_algorithm' [in Multiset]
K
key [in SearchTree]key [in Redblack]
kvs_insert [in SearchTree]
L
list_ind2 [in Merge]list_ind2_principle [in Merge]
list_nat_in [in Decide]
list_nat_eq_dec [in Decide]
List_Priqueue.Abs [in Priqueue]
List_Priqueue.priq [in Priqueue]
List_Priqueue.merge [in Priqueue]
List_Priqueue.delete_max [in Priqueue]
List_Priqueue.insert [in Priqueue]
List_Priqueue.empty [in Priqueue]
List_Priqueue.priqueue [in Priqueue]
List_Priqueue.key [in Priqueue]
List_Priqueue.select [in Priqueue]
list2map [in SearchTree]
look [in Trie]
lookup [in SearchTree]
lookup [in Trie]
lookup [in Redblack]
low_deg [in Color]
L.cons [in ADT]
L.create [in ADT]
L.list [in ADT]
L.nth [in ADT]
M
makeBlack [in Redblack]manual_grade_for_elements_spec [in SearchTree]
manual_grade_for_successor_of_Z_constant_time [in Trie]
manual_grade_for_permutations_vs_multiset [in BagPerm]
manual_grade_for_permutations_vs_multiset [in Multiset]
manual_grade_for_TreeTableModel2 [in ADT]
manual_grade_for_TreeTableModel [in ADT]
manual_grade_for_ListsETable [in ADT]
manual_grade_for_ListsTable [in ADT]
MapsTable.default [in ADT]
MapsTable.empty [in ADT]
MapsTable.get [in ADT]
MapsTable.key [in ADT]
MapsTable.set [in ADT]
MapsTable.table [in ADT]
MapsTable.V [in ADT]
Mdomain [in Color]
merge [in Merge]
mindepth [in Redblack]
mk_graph [in Color]
multiset [in Multiset]
N
nat2pos [in Trie]node [in Color]
nodemap [in Color]
nodes [in Color]
nodeset [in Color]
no_selfloop [in Color]
O
out_of_gas [in Selection]O_Abs [in ADT]
P
palette [in Color]pos2nat [in Trie]
PRIQUEUE.key [in Priqueue]
R
RatherSlow.collisions [in Trie]RatherSlow.collisions_pi [in Trie]
RatherSlow.empty [in Trie]
RatherSlow.loop [in Trie]
RatherSlow.total_mapz [in Trie]
RatherSlow.update [in Trie]
reflect_example2 [in Perm]
reflect_example1' [in Perm]
reflect_example1 [in Perm]
remove_node [in Color]
repeat [in ADT]
S
same_mod_10 [in Color]ScratchPad.is_3_less_7 [in Decide]
ScratchPad.lt_dec' [in Decide]
ScratchPad.lt_dec [in Decide]
ScratchPad.t1 [in Decide]
ScratchPad.t2 [in Decide]
ScratchPad.t4 [in Decide]
ScratchPad.v1a [in Decide]
ScratchPad.v1b [in Decide]
ScratchPad.v2a [in Decide]
ScratchPad.v3 [in Decide]
ScratchPad2.insert [in Decide]
ScratchPad2.le_dec [in Decide]
ScratchPad2.lt_dec [in Decide]
ScratchPad2.max_with_axiom [in Decide]
ScratchPad2.sort [in Decide]
SearchTree2.elements [in Extract]
SearchTree2.elements' [in Extract]
SearchTree2.empty_tree [in Extract]
SearchTree2.insert [in Extract]
SearchTree2.key [in Extract]
SearchTree2.lookup [in Extract]
SectionExample1.empty [in SearchTree]
SectionExample1.lookup [in SearchTree]
SectionExample1.mymap [in SearchTree]
SectionExample2.empty [in SearchTree]
SectionExample2.lookup [in SearchTree]
SectionExample2.mymap [in SearchTree]
select [in Selection]
selection_sort_correct [in Selection]
selection_sort [in Selection]
selsort [in Selection]
selsort [in Selection]
singleton [in Multiset]
sixlist [in ADT]
slow_elements [in SearchTree]
sort [in Sort]
sorted' [in Sort]
sorted'' [in Sort]
sort_pi [in Selection]
sort_pi [in Sort]
sort_pi_same_contents [in Multiset]
sort_pi [in Multiset]
Sort1.insert [in Extract]
Sort1.sort [in Extract]
split [in Merge]
step [in ADT]
stepish [in ADT]
subset_nodes [in Color]
T
TABLE.key [in ADT]three_ten [in Trie]
too_much_gas [in Selection]
TreeETable.default [in ADT]
TreeETable.elements [in ADT]
TreeETable.empty [in ADT]
TreeETable.get [in ADT]
TreeETable.key [in ADT]
TreeETable.set [in ADT]
TreeETable.table [in ADT]
TreeETable.V [in ADT]
TreeETable2.default [in ADT]
TreeETable2.elements [in ADT]
TreeETable2.empty [in ADT]
TreeETable2.get [in ADT]
TreeETable2.key [in ADT]
TreeETable2.set [in ADT]
TreeETable2.table [in ADT]
TreeETable2.V [in ADT]
TreeETable3.default [in ADT]
TreeETable3.elements [in ADT]
TreeETable3.empty [in ADT]
TreeETable3.get [in ADT]
TreeETable3.is_table [in ADT]
TreeETable3.key [in ADT]
TreeETable3.set [in ADT]
TreeETable3.table [in ADT]
TreeETable3.V [in ADT]
TreeTable.default [in ADT]
TreeTable.elements [in ADT]
TreeTable.empty [in ADT]
TreeTable.get [in ADT]
TreeTable.key [in ADT]
TreeTable.set [in ADT]
TreeTable.table [in ADT]
TreeTable.V [in ADT]
tree2map [in SearchTree]
trie_table [in Trie]
U
undirected [in Color]union [in SearchTree]
union [in Multiset]
V
value [in Multiset]VerySlow.collisions [in Trie]
VerySlow.collisions_pi [in Trie]
VerySlow.loop [in Trie]
| 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 | (750 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 | (5 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 | (31 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 | (13 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 | (16 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 | (265 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 | (44 entries) |
| Axiom 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 | (82 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 | (21 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 | (6 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 | (267 entries) |
This page has been generated by coqdoc