Global Index

J

X

Y

_

(997 entries)

Notation Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(7 entries)

Module Index

A

C

D

G

H

J

K

U

X

Y

Z

_

other

(55 entries)

Library Index

F

G

H

I

J

K

L

N

O

Q

U

V

W

X

Y

Z

_

other

(17 entries)

Lemma Index

D

H

J

O

Q

W

X

Y

_

other

(330 entries)

Constructor Index

A

C

D

F

G

H

J

K

M

O

P

Q

U

V

W

X

Y

Z

_

other

(49 entries)

Axiom Index

B

C

D

F

G

H

J

K

M

N

O

R

U

W

X

Y

Z

_

other

(105 entries)

Inductive Index

A

D

E

F

G

H

J

K

M

O

P

Q

U

V

W

X

Y

Z

_

other

(23 entries)

Definition Index

J

Q

W

X

Y

Z

_

other

(411 entries)

Global Index

A

Abs [definition, in Trie]
Abs [definition, in SearchTree]
Abs [axiom, in Extract]
abstract [definition, in Trie]
Abs_three_ten [definition, in Trie]
Abs_inj [axiom, in Extract]
Abs' [definition, in SearchTree]
add_edge [definition, in Color]
adj [definition, in Color]
adj_ext [lemma, in Color]
ADT [library]
apply_empty [lemma, in Maps]
a_vector [definition, 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_sind [definition, in Binom]
BinomQueue.priqueue_elems_rec [definition, in Binom]
BinomQueue.priqueue_elems_ind [definition, in Binom]
BinomQueue.priqueue_elems_rect [definition, 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_sind [definition, in Binom]
BinomQueue.tree_elems_ind [definition, in Binom]
BinomQueue.tree_elems_node [constructor, in Binom]
BinomQueue.tree_elems_leaf [constructor, in Binom]
BinomQueue.tree_elems [inductive, in Binom]
BinomQueue.tree_sind [definition, in Binom]
BinomQueue.tree_rec [definition, in Binom]
BinomQueue.tree_ind [definition, in Binom]
BinomQueue.tree_rect [definition, in Binom]
BinomQueue.unzip [definition, in Binom]
Black [constructor, in Redblack]
bound [definition, in SearchTree]
bound_relate' [lemma, in SearchTree]
bound_relate [lemma, in SearchTree]
bound_value [lemma, in SearchTree]
bound_default [lemma, in SearchTree]
BST [inductive, in Redblack]
BST [inductive, in SearchTree]
BST_sind [definition, in Redblack]
BST_ind [definition, in Redblack]
BST_sind [definition, in SearchTree]
BST_ind [definition, in SearchTree]
BST_T [constructor, in SearchTree]
BST_E [constructor, in SearchTree]
butterfly [definition, in Perm]

C

cardinal_map [lemma, in Color]
color [inductive, in Redblack]
color [definition, in Color]
Color [library]
coloring [definition, in Color]
coloring_ok [definition, in Color]
colors_of [definition, in Color]
color_sind [definition, in Redblack]
color_rec [definition, in Redblack]
color_ind [definition, in Redblack]
color_rect [definition, in Redblack]
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_of_small_maintains_sort' [lemma, in Selection]
cons_of_small_maintains_sort [lemma, in Selection]
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]

D

Decide [library]
disjoint [definition, in SearchTree]
domain_example_map [definition, in Color]

E

E [constructor, in Redblack]
E [module, in Color]
E [constructor, in SearchTree]
E [constructor, in Extract]
elements [definition, in Redblack]
elements [definition, in SearchTree]
elements [definition, in Extract]
elements_aux [definition, in Redblack]
elements_relate' [lemma, in SearchTree]
elements_relate [lemma, in SearchTree]
elements_empty [lemma, in SearchTree]
elements_nodup_keys [lemma, in SearchTree]
elements_correct_inverse [lemma, in SearchTree]
elements_complete_inverse [lemma, in SearchTree]
elements_correct [lemma, in SearchTree]
elements_preserves_relation [lemma, in SearchTree]
elements_preserves_forall [lemma, in SearchTree]
elements_correct_spec [definition, in SearchTree]
elements_complete [lemma, in SearchTree]
elements_complete_spec [definition, in SearchTree]
elements_complete_broken [lemma, in SearchTree]
elements_complete_broken_spec [definition, in SearchTree]
elements_ex [definition, in SearchTree]
elements_aux [definition, in Extract]
empty [definition, in Trie]
empty [definition, in Multiset]
empty [definition, in Maps]
empty_relate [lemma, in Trie]
empty_is_trie [lemma, in Trie]
empty_tree_BST [lemma, in Redblack]
empty_tree [definition, in Redblack]
empty_relate' [lemma, in SearchTree]
empty_relate [lemma, in SearchTree]
empty_tree_BST [lemma, in SearchTree]
empty_tree [definition, in SearchTree]
empty_map [definition, in ADT]
empty_tree [definition, in Extract]
eqb_reflect [lemma, in Perm]
eqlistA_Eeq_eq [lemma, in Color]
equivlistA_example [definition, in Color]
ETable [module, in ADT]
ETableAbs [module, in ADT]
ETableAbs.Abs [axiom, in ADT]
ETableAbs.bound [axiom, in ADT]
ETableAbs.bound_relate [axiom, in ADT]
ETableAbs.default [axiom, in ADT]
ETableAbs.elements [axiom, in ADT]
ETableAbs.elements_relate [axiom, in ADT]
ETableAbs.empty [axiom, in ADT]
ETableAbs.empty_relate [axiom, in ADT]
ETableAbs.empty_ok [axiom, in ADT]
ETableAbs.get [axiom, in ADT]
ETableAbs.insert_relate [axiom, in ADT]
ETableAbs.key [definition, in ADT]
ETableAbs.lookup_relate [axiom, in ADT]
ETableAbs.rep_ok [axiom, in ADT]
ETableAbs.set [axiom, in ADT]
ETableAbs.set_ok [axiom, in ADT]
ETableAbs.table [axiom, in ADT]
ETableAbs.V [axiom, in ADT]
ETableSubset [module, in ADT]
ETableSubset.bound [axiom, in ADT]
ETableSubset.bound_set_other [axiom, in ADT]
ETableSubset.bound_set_same [axiom, in ADT]
ETableSubset.bound_empty [axiom, in ADT]
ETableSubset.elements [axiom, in ADT]
ETableSubset.elements_correct [axiom, in ADT]
ETableSubset.elements_complete [axiom, in ADT]
ETable_first_attempt.elements_correct [axiom, in ADT]
ETable_first_attempt.elements_complete [axiom, in ADT]
ETable_first_attempt.elements [axiom, in ADT]
ETable_first_attempt.bound [axiom, in ADT]
ETable_first_attempt [module, in ADT]
ETable.bound [axiom, in ADT]
ETable.bound_set_other [axiom, in ADT]
ETable.bound_set_same [axiom, in ADT]
ETable.bound_empty [axiom, in ADT]
ETable.elements [axiom, in ADT]
ETable.elements_correct [axiom, in ADT]
ETable.elements_complete [axiom, in ADT]
ETable.empty_ok [axiom, in ADT]
ETable.rep_ok [axiom, in ADT]
ETable.set_ok [axiom, in ADT]
even_nat [definition, in ADT]
Even2 [lemma, in ADT]
Even2' [definition, in ADT]
examplemap [definition, in Maps]
example_map [definition, in Color]
exposed_trees_ex [definition, in ADT]
Extract [library]
extra_fuel [definition, in Selection]
ex_tree [definition, in SearchTree]

F

FastEnough [module, in Trie]
FastEnough.collisions [definition, in Trie]
FastEnough.collisions_pi [definition, in Trie]
FastEnough.loop [definition, in Trie]
fast_elements_correct [lemma, in SearchTree]
fast_elements_eq_elements [lemma, in SearchTree]
fast_elements_tr_helper [lemma, in SearchTree]
fast_elements [definition, in SearchTree]
fast_elements_tr [definition, in SearchTree]
filter_sortE [lemma, in Color]
find [definition, in SearchTree]
first_le_second [definition, in Perm]
fold_right_rev_left [lemma, in Color]
ForallT [definition, in Redblack]
ForallT [definition, in SearchTree]
ForallT_less [lemma, in Redblack]
ForallT_greater [lemma, in Redblack]
ForallT_imp [lemma, in Redblack]
ForallT_insert [lemma, in SearchTree]
Forall_perm [lemma, in Perm]
FunTable [module, in ADT]
FunTableExamples [module, in ADT]
FunTableExamples.ex1 [definition, in ADT]
FunTableExamples.ex2 [definition, in ADT]
FunTableExamples.ex3 [definition, in ADT]
FunTableExamples.StringFunTable [module, in ADT]
FunTable.default [definition, in ADT]
FunTable.empty [definition, in ADT]
FunTable.get [definition, in ADT]
FunTable.get_set_other [lemma, in ADT]
FunTable.get_set_same [lemma, in ADT]
FunTable.get_empty_default [lemma, in ADT]
FunTable.key [definition, in ADT]
FunTable.set [definition, in ADT]
FunTable.table [definition, in ADT]
FunTable.V [definition, in ADT]

G

G [definition, in Color]
geb [definition, in Perm]
geb_reflect [lemma, in Perm]
graph [definition, in Color]
gtb [definition, in Perm]
gtb_reflect [lemma, in Perm]

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]
ins [definition, in Extract]
insert [definition, in Trie]
insert [definition, in Redblack]
insert [definition, in SearchTree]
insert [definition, in Sort]
insert [definition, in Extract]
insertion_sort_correct [lemma, in Sort]
insertion_sort_correct [lemma, in BagPerm]
insertion_sort_correct [lemma, in Multiset]
insert_relate [lemma, in Trie]
insert_is_trie [lemma, in Trie]
insert_RB [lemma, in Redblack]
insert_BST [lemma, in Redblack]
insert_BST [lemma, in Redblack]
insert_relate' [lemma, in SearchTree]
insert_relate [lemma, in SearchTree]
insert_permute_equality_breaks [lemma, in SearchTree]
insert_same_equality_breaks [lemma, in SearchTree]
insert_shadow_equality [lemma, in SearchTree]
insert_BST [lemma, in SearchTree]
insert_sorted' [lemma, in Sort]
insert_perm [lemma, in Sort]
insert_sorted [lemma, in Sort]
insert_bag [lemma, in BagPerm]
insert_contents [lemma, in Multiset]
insP [lemma, in Redblack]
insZ [definition, in Extract]
ins_red [lemma, in Redblack]
ins_RB [lemma, in Redblack]
ins_BST [lemma, in Redblack]
ins_not_E [lemma, in Redblack]
ins_not_E [lemma, in Redblack]
ins_int [definition, in Extract]
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.comparison_sind [definition, in Trie]
Integers.comparison_rec [definition, in Trie]
Integers.comparison_ind [definition, in Trie]
Integers.comparison_rect [definition, in Trie]
Integers.Eq [constructor, in Trie]
Integers.Gt [constructor, in Trie]
Integers.Lt [constructor, in Trie]
Integers.positive [inductive, in Trie]
Integers.positive_sind [definition, in Trie]
Integers.positive_rec [definition, in Trie]
Integers.positive_ind [definition, in Trie]
Integers.positive_rect [definition, 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.Z_sind [definition, in Trie]
Integers.Z_rec [definition, in Trie]
Integers.Z_ind [definition, in Trie]
Integers.Z_rect [definition, in Trie]
Integers.Z0 [constructor, in Trie]
_ ~ 0 [notation, in Trie]
_ ~ 1 [notation, in Trie]
int_leb_reflect [lemma, in Extract]
int_ltb_reflect [lemma, in Extract]
in_colors_of_1 [lemma, in Color]
in_map_of_list [lemma, in SearchTree]
in_fst [lemma, in SearchTree]
in_4_pi [definition, in Decide]
is_trie [definition, in Trie]
is_BST_ex [definition, in SearchTree]
is_a_sorting_algorithm [definition, in Sort]
is_a_sorting_algorithm' [definition, in BagPerm]
is_a_sorting_algorithm [definition, in Selection]
is_a_sorting_algorithm' [definition, in Multiset]

K

key [definition, in Redblack]
key [definition, in SearchTree]
key [definition, in Extract]
kvs_insert_elements [lemma, in SearchTree]
kvs_insert_split [lemma, in SearchTree]
kvs_insert [definition, in SearchTree]

L

Leaf [constructor, in Trie]
leb [axiom, in Extract]
leb_reflect [lemma, in Perm]
leb_le [axiom, in Extract]
le_all__le_one [lemma, in Selection]
le_all [definition, in Selection]
lia_example_3 [lemma, in Perm]
lia_example2 [lemma, in Perm]
lia_example1 [lemma, in Perm]
lia_example1 [lemma, in Perm]
ListETableAbs [module, in ADT]
ListETableAbs.Abs [definition, in ADT]
ListETableAbs.bound [definition, in ADT]
ListETableAbs.bound_relate [lemma, in ADT]
ListETableAbs.default [definition, in ADT]
ListETableAbs.elements [definition, in ADT]
ListETableAbs.elements_relate [lemma, in ADT]
ListETableAbs.empty [definition, in ADT]
ListETableAbs.empty_relate [lemma, in ADT]
ListETableAbs.empty_ok [lemma, in ADT]
ListETableAbs.get [definition, in ADT]
ListETableAbs.insert_relate [lemma, in ADT]
ListETableAbs.key [definition, in ADT]
ListETableAbs.lookup_relate [lemma, in ADT]
ListETableAbs.rep_ok [definition, in ADT]
ListETableAbs.set [definition, in ADT]
ListETableAbs.set_ok [lemma, in ADT]
ListETableAbs.table [definition, in ADT]
ListETableAbs.V [definition, in ADT]
ListQueue [module, in ADT]
ListQueue.deq [definition, in ADT]
ListQueue.deq_nonempty [lemma, in ADT]
ListQueue.deq_empty [lemma, in ADT]
ListQueue.empty [definition, in ADT]
ListQueue.enq [definition, in ADT]
ListQueue.is_empty_nonempty [lemma, in ADT]
ListQueue.is_empty_empty [lemma, in ADT]
ListQueue.is_empty [definition, in ADT]
ListQueue.peek [definition, in ADT]
ListQueue.peek_nonempty [lemma, in ADT]
ListQueue.peek_empty [lemma, in ADT]
ListQueue.queue [definition, in ADT]
ListQueue.V [definition, in ADT]
ListsTable [module, in ADT]
ListsTable.default [definition, in ADT]
ListsTable.empty [definition, in ADT]
ListsTable.get [definition, in ADT]
ListsTable.get_set_other [lemma, in ADT]
ListsTable.get_set_same [lemma, in ADT]
ListsTable.get_empty_default [lemma, in ADT]
ListsTable.key [definition, in ADT]
ListsTable.set [definition, in ADT]
ListsTable.table [definition, in ADT]
ListsTable.V [definition, in ADT]
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'_sind [definition, in Priqueue]
List_Priqueue.Abs'_ind [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]
list_keys [definition, in SearchTree]
list_nat_in [definition, in Decide]
list_nat_eq_dec [definition, in Decide]
list_of_vector [definition, in ADT]
list_ind2 [definition, in Merge]
list_ind2_principle [definition, in Merge]
look [definition, in Trie]
lookup [definition, in Trie]
lookup [definition, in Redblack]
lookup [definition, in SearchTree]
lookup [definition, in Extract]
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]
lookup_relate' [lemma, in SearchTree]
lookup_relate [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_eq' [lemma, in SearchTree]
lookup_insert_eq [lemma, in SearchTree]
lookup_empty [lemma, in SearchTree]
lookup_insert_neq [lemma, in Extract]
lookup_insert_eq [lemma, in Extract]
lookup_empty [lemma, in Extract]
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]

M

M [module, in Color]
make_black [definition, in Redblack]
manual_grade_for_successor_of_Z_constant_time [definition, in Trie]
manual_grade_for_redblack_bound [definition, in Redblack]
manual_grade_for_bound_correct [definition, in SearchTree]
manual_grade_for_permutations_vs_multiset [definition, in BagPerm]
manual_grade_for_ListsETable [definition, in ADT]
manual_grade_for_TreeTableModel [definition, in ADT]
Maps [library]
map_of_list_app [lemma, in SearchTree]
map_of_tree_prop [lemma, in SearchTree]
map_of_tree [definition, in SearchTree]
map_bound [definition, in SearchTree]
map_of_list [definition, in SearchTree]
map_find [definition, in ADT]
map_update [definition, in ADT]
maybe_swap_correct [lemma, in Perm]
maybe_swap_perm [lemma, in Perm]
maybe_swap_idempotent [lemma, in Perm]
maybe_swap_idempotent [lemma, in Perm]
maybe_swap_321 [definition, in Perm]
maybe_swap_123 [definition, in Perm]
maybe_swap [definition, in Perm]
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

NatFunTableExamples [module, in ADT]
nat2pos [definition, in Trie]
nat2pos_injective [lemma, in Trie]
nat2pos2nat [lemma, in Trie]
NearlyRB [inductive, in Redblack]
NearlyRB_sind [definition, in Redblack]
NearlyRB_ind [definition, in Redblack]
NearlyRB_b [constructor, in Redblack]
NearlyRB_r [constructor, in Redblack]
NicelyEncapsulatedExample [module, in ADT]
NicelyEncapsulatedExample.ex1 [definition, in ADT]
NicelyEncapsulatedExample.ex2 [definition, in ADT]
NicelyEncapsulatedExample.StringTreeETableEncapsulated [module, in ADT]
Node [constructor, in Trie]
node [definition, in Color]
nodemap [definition, in Color]
nodes [definition, in Color]
nodeset [definition, in Color]
NoDup_append [lemma, in SearchTree]
NotBst [module, in SearchTree]
NotBst.not_bst_lookup_wrong [definition, in SearchTree]
NotBst.t [definition, in SearchTree]
not_in_map_of_list [lemma, in SearchTree]
not_BST_ex [definition, in SearchTree]
not_a_permutation [definition, in Perm]
no_selfloop [definition, in Color]
nth_error_insert [lemma, in Sort]

O

out_of_fuel [definition, in Selection]
OverlyEncapsulatedExample [module, in ADT]
OverlyEncapsulatedExample.ex1 [definition, in ADT]
OverlyEncapsulatedExample.StringTreeETableFullyEncapsulated [module, in ADT]

P

pairs_example [definition, in Selection]
palette [definition, in Color]
partial_map [definition, in Maps]
Perm [library]
permut_example [definition, in Perm]
perm_bag [lemma, in BagPerm]
perm_contents [lemma, in Multiset]
plus_two [definition, in ADT]
plus_two [definition, in ADT]
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]

Q

Queue [module, in ADT]
QueueAbs [module, in ADT]
QueueAbs.Abs [axiom, in ADT]
QueueAbs.deq [axiom, in ADT]
QueueAbs.deq_relate [axiom, in ADT]
QueueAbs.empty [axiom, in ADT]
QueueAbs.empty_relate [axiom, in ADT]
QueueAbs.enq [axiom, in ADT]
QueueAbs.enq_relate [axiom, in ADT]
QueueAbs.is_empty [axiom, in ADT]
QueueAbs.peek [axiom, in ADT]
QueueAbs.peek_relate [axiom, in ADT]
QueueAbs.queue [axiom, in ADT]
QueueAbs.V [axiom, in ADT]
Queue.deq [axiom, in ADT]
Queue.deq_nonempty [axiom, in ADT]
Queue.deq_empty [axiom, in ADT]
Queue.empty [axiom, in ADT]
Queue.enq [axiom, in ADT]
Queue.is_empty_nonempty [axiom, in ADT]
Queue.is_empty_empty [axiom, in ADT]
Queue.is_empty [axiom, in ADT]
Queue.peek [axiom, in ADT]
Queue.peek_nonempty [axiom, in ADT]
Queue.peek_empty [axiom, in ADT]
Queue.queue [axiom, in ADT]
Queue.V [axiom, in ADT]

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]
RB [inductive, in Redblack]
RB_blacken_root [lemma, in Redblack]
RB_blacken_parent [lemma, in Redblack]
RB_sind [definition, in Redblack]
RB_ind [definition, in Redblack]
RB_b [constructor, in Redblack]
RB_r [constructor, in Redblack]
RB_leaf [constructor, in Redblack]
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]

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.sumbool_sind [definition, in Decide]
ScratchPad.sumbool_rec [definition, in Decide]
ScratchPad.sumbool_ind [definition, in Decide]
ScratchPad.sumbool_rect [definition, 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_sind [definition, in Decide]
ScratchPad2.sorted_ind [definition, in Decide]
ScratchPad2.sorted_cons [constructor, in Decide]
ScratchPad2.sorted_1 [constructor, in Decide]
ScratchPad2.sorted_nil [constructor, in Decide]
SearchTree [library]
select [definition, in Selection]
Selection [library]
selection_sort_correct' [lemma, in Selection]
selection_sort_contents [lemma, in Selection]
selection_sort_is_correct [lemma, in Selection]
selection_sort_sorted [lemma, in Selection]
selection_sort_perm [lemma, in Selection]
selection_sort [definition, in Selection]
select_terminates [lemma, in Color]
select_contents [lemma, in Selection]
select_in [lemma, in Selection]
select_smallest [lemma, in Selection]
select_fst_leq [lemma, in Selection]
select_rest_length [lemma, in Selection]
select_perm [lemma, in Selection]
selsort [definition, in Selection]
selsort [definition, in Selection]
selsort_sorted [lemma, in Selection]
selsort_perm [lemma, in Selection]
selsort'_is_correct [lemma, in Selection]
selsort'_sorted [lemma, in Selection]
selsort'_perm [lemma, in Selection]
selsort'_example [definition, in Selection]
SigSandbox [module, in ADT]
SigSandbox.ex [inductive, in ADT]
SigSandbox.exist [constructor, in ADT]
SigSandbox.ex_sind [definition, in ADT]
SigSandbox.ex_ind [definition, in ADT]
SigSandbox.ex_intro [constructor, in ADT]
SigSandbox.proj1_ex [definition, in ADT]
SigSandbox.proj1_sig [definition, in ADT]
SigSandbox.proj2_sig [definition, in ADT]
SigSandbox.sig [inductive, in ADT]
SigSandbox.sig_sind [definition, in ADT]
SigSandbox.sig_rec [definition, in ADT]
SigSandbox.sig_ind [definition, in ADT]
SigSandbox.sig_rect [definition, in ADT]
{ _ : _ | _ } [notation, in ADT]
SimpleStringTable1 [module, in ADT]
SimpleStringTable1.default [definition, in ADT]
SimpleStringTable1.key [definition, in ADT]
SimpleStringTable1.table [definition, in ADT]
SimpleStringTable1.V [definition, in ADT]
SimpleStringTable2 [module, in ADT]
SimpleStringTable2.default [definition, in ADT]
SimpleStringTable2.key [definition, in ADT]
SimpleStringTable2.table [definition, in ADT]
SimpleStringTable2.V [definition, in ADT]
SimpleStringTable3 [module, in ADT]
SimpleStringTable3.default [definition, in ADT]
SimpleStringTable3.key [definition, in ADT]
SimpleStringTable3.table [definition, in ADT]
SimpleStringTable3.V [definition, in ADT]
SimpleTable [module, in ADT]
SimpleTable.default [axiom, in ADT]
SimpleTable.key [axiom, in ADT]
SimpleTable.table [axiom, in ADT]
SimpleTable.V [axiom, in ADT]
SimpleTable2 [module, in ADT]
SimpleTable3 [module, in ADT]
singleton [definition, in Multiset]
Sin_domain [lemma, in Color]
Snot_in_empty [lemma, in Color]
sort [definition, in Sort]
sort [definition, in Extract]
Sort [library]
sorted [inductive, in Sort]
sorted [inductive, in Selection]
sorted [inductive, in Extract]
Sorted_lt_key [lemma, in Color]
sorted_elements [lemma, in SearchTree]
sorted_app [lemma, in SearchTree]
sorted_sorted' [lemma, in Sort]
sorted_sind [definition, in Sort]
sorted_ind [definition, in Sort]
sorted_cons [constructor, in Sort]
sorted_1 [constructor, in Sort]
sorted_nil [constructor, in Sort]
sorted_iff_sorted [lemma, in Selection]
sorted_sind [definition, in Selection]
sorted_ind [definition, in Selection]
sorted_cons [constructor, in Selection]
sorted_1 [constructor, in Selection]
sorted_nil [constructor, in Selection]
sorted_merge [lemma, in Merge]
sorted_merge1 [lemma, in Merge]
sorted_sind [definition, in Extract]
sorted_ind [definition, in Extract]
sorted_cons [constructor, in Extract]
sorted_1 [constructor, in Extract]
sorted_nil [constructor, in Extract]
sorted' [definition, in Sort]
sorted'_sorted [lemma, in Sort]
sorted'' [definition, in Sort]
SortE_equivlistE_eqlistE [lemma, in Color]
sortZ [definition, in Extract]
sort_sorted' [lemma, in Sort]
sort_perm [lemma, in Sort]
sort_sorted [lemma, in Sort]
sort_pi [definition, in Sort]
sort_specifications_equivalent [lemma, in BagPerm]
sort_bag [lemma, in BagPerm]
sort_pi [definition, in Selection]
sort_specifications_equivalent [lemma, in Multiset]
sort_contents [lemma, in Multiset]
sort_pi_same_contents [definition, in Multiset]
sort_int_correct [lemma, in Extract]
sort_int [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]
StringListETableAbs [module, in ADT]
StringListsTableExamples [module, in ADT]
StringListsTableExamples.ex1 [definition, in ADT]
StringListsTableExamples.ex2 [definition, in ADT]
StringListsTableExamples.ex3 [definition, in ADT]
StringListsTableExamples.StringListsTable [module, in ADT]
StringTreeETableExample [module, in ADT]
StringTreeETableExample.ex1 [definition, in ADT]
StringTreeETableExample.StringTreeETable [module, in ADT]
StringVal [module, in ADT]
StringVal.default [definition, in ADT]
StringVal.V [definition, in ADT]
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 Redblack]
T [constructor, in SearchTree]
T [constructor, in Extract]
Table [module, in ADT]
Table.default [axiom, in ADT]
Table.empty [axiom, in ADT]
Table.get [axiom, in ADT]
Table.get_set_other [axiom, in ADT]
Table.get_set_same [axiom, in ADT]
Table.get_empty_default [axiom, in ADT]
Table.key [definition, in ADT]
Table.set [axiom, in ADT]
Table.table [axiom, in ADT]
Table.V [axiom, in ADT]
Tests [module, in SearchTree]
Tests.bst_ex₄ [definition, in SearchTree]
Tests.bst_ex₃ [definition, in SearchTree]
Tests.bst_ex₂ [definition, in SearchTree]
Tests.bst_ex₁ [definition, in SearchTree]
three_ten [definition, in Trie]
three_less_seven_2 [lemma, in Decide]
three_less_seven_1 [lemma, in Decide]
total_map [definition, in Maps]
tree [inductive, in Redblack]
tree [inductive, in SearchTree]
tree [inductive, in Extract]
TreeETable [module, in ADT]
TreeETableEncapsulated [module, in ADT]
TreeETableEncapsulated.bound [definition, in ADT]
TreeETableEncapsulated.bound_set_other [lemma, in ADT]
TreeETableEncapsulated.bound_set_same [lemma, in ADT]
TreeETableEncapsulated.bound_empty [lemma, in ADT]
TreeETableEncapsulated.elements [definition, in ADT]
TreeETableEncapsulated.elements_correct [lemma, in ADT]
TreeETableEncapsulated.elements_complete [lemma, in ADT]
TreeETableEncapsulated.empty_ok [lemma, in ADT]
TreeETableEncapsulated.rep_ok [definition, in ADT]
TreeETableEncapsulated.set_ok [lemma, in ADT]
TreeETableFullyEncapsulated [module, in ADT]
TreeETableFullyEncapsulated.bound [definition, in ADT]
TreeETableFullyEncapsulated.bound_set_other [lemma, in ADT]
TreeETableFullyEncapsulated.bound_set_same [lemma, in ADT]
TreeETableFullyEncapsulated.bound_empty [lemma, in ADT]
TreeETableFullyEncapsulated.elements [definition, in ADT]
TreeETableFullyEncapsulated.elements_correct [lemma, in ADT]
TreeETableFullyEncapsulated.elements_complete [lemma, in ADT]
TreeETableFullyEncapsulated.empty_ok [lemma, in ADT]
TreeETableFullyEncapsulated.rep_ok [definition, in ADT]
TreeETableFullyEncapsulated.set_ok [lemma, in ADT]
TreeETableSubset [module, in ADT]
TreeETableSubset.bound [definition, in ADT]
TreeETableSubset.bound_set_other [lemma, in ADT]
TreeETableSubset.bound_set_same [lemma, in ADT]
TreeETableSubset.bound_empty [lemma, in ADT]
TreeETableSubset.default [definition, in ADT]
TreeETableSubset.elements [definition, in ADT]
TreeETableSubset.elements_correct [lemma, in ADT]
TreeETableSubset.elements_complete [lemma, in ADT]
TreeETableSubset.empty [definition, in ADT]
TreeETableSubset.get [definition, in ADT]
TreeETableSubset.get_set_other [lemma, in ADT]
TreeETableSubset.get_set_same [lemma, in ADT]
TreeETableSubset.get_empty_default [lemma, in ADT]
TreeETableSubset.key [definition, in ADT]
TreeETableSubset.set [definition, in ADT]
TreeETableSubset.table [definition, in ADT]
TreeETableSubset.V [definition, in ADT]
TreeETable_first_attempt.elements_correct [lemma, in ADT]
TreeETable_first_attempt.elements_complete [lemma, in ADT]
TreeETable_first_attempt.elements [definition, in ADT]
TreeETable_first_attempt.bound [definition, in ADT]
TreeETable_first_attempt [module, in ADT]
TreeETable.bound [definition, in ADT]
TreeETable.bound_set_other [lemma, in ADT]
TreeETable.bound_set_same [lemma, in ADT]
TreeETable.bound_empty [lemma, in ADT]
TreeETable.elements [definition, in ADT]
TreeETable.elements_correct [lemma, in ADT]
TreeETable.elements_complete [lemma, in ADT]
TreeETable.empty_ok [lemma, in ADT]
TreeETable.rep_ok [definition, in ADT]
TreeETable.set_ok [lemma, in ADT]
TreeTable [module, in ADT]
TreeTable.default [definition, in ADT]
TreeTable.empty [definition, in ADT]
TreeTable.get [definition, in ADT]
TreeTable.get_set_other [lemma, in ADT]
TreeTable.get_set_same [lemma, in ADT]
TreeTable.get_empty_default [lemma, in ADT]
TreeTable.key [definition, in ADT]
TreeTable.set [definition, in ADT]
TreeTable.table [definition, in ADT]
TreeTable.V [definition, in ADT]
tree_sind [definition, in Redblack]
tree_rec [definition, in Redblack]
tree_ind [definition, in Redblack]
tree_rect [definition, in Redblack]
tree_sind [definition, in SearchTree]
tree_rec [definition, in SearchTree]
tree_ind [definition, in SearchTree]
tree_rect [definition, in SearchTree]
tree_sind [definition, in Extract]
tree_rec [definition, in Extract]
tree_ind [definition, in Extract]
tree_rect [definition, in Extract]
trie [inductive, in Trie]
Trie [library]
trie_table [definition, in Trie]
trie_sind [definition, in Trie]
trie_rec [definition, in Trie]
trie_ind [definition, in Trie]
trie_rect [definition, in Trie]
truncated_subtraction [lemma, in Perm]
two [definition, in ADT]
two [definition, in ADT]
TwoListQueueAbs [module, in ADT]
TwoListQueueAbs.Abs [definition, in ADT]
TwoListQueueAbs.deq [definition, in ADT]
TwoListQueueAbs.deq_relate [lemma, in ADT]
TwoListQueueAbs.empty [definition, in ADT]
TwoListQueueAbs.empty_relate [lemma, in ADT]
TwoListQueueAbs.enq [definition, in ADT]
TwoListQueueAbs.enq_relate [lemma, in ADT]
TwoListQueueAbs.is_empty [definition, in ADT]
TwoListQueueAbs.peek [definition, in ADT]
TwoListQueueAbs.peek_relate [lemma, in ADT]
TwoListQueueAbs.queue [definition, in ADT]
TwoListQueueAbs.V [definition, in ADT]
two' [definition, in ADT]
t_update_permute [lemma, in Maps]
t_update_same [lemma, in Maps]
t_update_shadow [lemma, in Maps]
t_update_neq [lemma, in Maps]
t_update_eq [lemma, in Maps]
t_apply_empty [lemma, in Maps]
t_update [definition, in Maps]
t_empty [definition, in Maps]

U

uncurry [definition, in SearchTree]
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_swap [lemma, in Multiset]
union_comm [lemma, in Multiset]
union_assoc [lemma, in Multiset]
Unnamed_thm [definition, in Trie]
Unnamed_thm0 [definition, in Color]
Unnamed_thm [definition, in Color]
Unnamed_thm [definition, in Decide]
update [definition, in Maps]
update_permute [lemma, in Maps]
update_same [lemma, in Maps]
update_shadow [lemma, in Maps]
update_neq [lemma, in Maps]
update_eq [lemma, in Maps]
update_example4 [definition, in Maps]
update_example3 [definition, in Maps]
update_example2 [definition, in Maps]
update_example1 [definition, in Maps]

V

ValType [module, in ADT]
ValType.default [axiom, in ADT]
ValType.V [axiom, in ADT]
value [definition, in Multiset]
vector [definition, in ADT]
vector_app_correct [lemma, in ADT]
vector_app [definition, in ADT]
vector_cons_correct [lemma, in ADT]
vector_cons [definition, in ADT]
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_geb_reflect [lemma, in Extract]
Z_gtb_reflect [lemma, in Extract]
Z_leb_reflect [lemma, in Extract]
Z_ltb_reflect [lemma, in Extract]
Z_eqb_reflect [lemma, in Extract]

other

_ >? _ (nat_scope) [notation, in Perm]
_ >=? _ (nat_scope) [notation, in Perm]
_ <=* _ [notation, in Selection]

Notation Index

I

_ ~ 0 [in Trie]
_ ~ 1 [in Trie]

S

{ _ } + { _ } (type_scope) [in Decide]
{ _ : _ | _ } [in ADT]

other

_ >? _ (nat_scope) [in Perm]
_ >=? _ (nat_scope) [in Perm]
_ <=* _ [in Selection]

Module Index

B

BinomQueue [in Binom]

E

E [in Color]
ETable [in ADT]
ETableAbs [in ADT]
ETableSubset [in ADT]
ETable_first_attempt [in ADT]

F

FastEnough [in Trie]
FunTable [in ADT]
FunTableExamples [in ADT]
FunTableExamples.StringFunTable [in ADT]

I

Integers [in Trie]

L

ListETableAbs [in ADT]
ListQueue [in ADT]
ListsTable [in ADT]
List_Priqueue [in Priqueue]

M

M [in Color]

N

NatFunTableExamples [in ADT]
NicelyEncapsulatedExample [in ADT]
NicelyEncapsulatedExample.StringTreeETableEncapsulated [in ADT]
NotBst [in SearchTree]

O

OverlyEncapsulatedExample [in ADT]
OverlyEncapsulatedExample.StringTreeETableFullyEncapsulated [in ADT]

P

PRIQUEUE [in Priqueue]

Q

Queue [in ADT]
QueueAbs [in ADT]

R

RatherSlow [in Trie]

S

S [in Color]
ScratchPad [in Decide]
ScratchPad2 [in Decide]
SigSandbox [in ADT]
SimpleStringTable1 [in ADT]
SimpleStringTable2 [in ADT]
SimpleStringTable3 [in ADT]
SimpleTable [in ADT]
SimpleTable2 [in ADT]
SimpleTable3 [in ADT]
StringListETableAbs [in ADT]
StringListsTableExamples [in ADT]
StringListsTableExamples.StringListsTable [in ADT]
StringTreeETableExample [in ADT]
StringTreeETableExample.StringTreeETable [in ADT]
StringVal [in ADT]

T

Table [in ADT]
Tests [in SearchTree]
TreeETable [in ADT]
TreeETableEncapsulated [in ADT]
TreeETableFullyEncapsulated [in ADT]
TreeETableSubset [in ADT]
TreeETable_first_attempt [in ADT]
TreeTable [in ADT]
TwoListQueueAbs [in ADT]

V

ValType [in ADT]
VerySlow [in Trie]

W

WF [in Color]
WP [in Color]

Library Index

A

ADT

B

C

Color

D

Decide

E

M

Maps
Merge
Multiset

P

Perm
Preface
Priqueue

R

S

SearchTree
Selection
Sort

T

Trie

Lemma Index

A

adj_ext [in Color]
apply_empty [in Maps]

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]
bound_relate' [in SearchTree]
bound_relate [in SearchTree]
bound_value [in SearchTree]
bound_default [in SearchTree]

C

cardinal_map [in Color]
color_correct [in Color]
compute_with_StdLib_lt_dec [in Decide]
compute_with_lt_dec [in Decide]
cons_of_small_maintains_sort' [in Selection]
cons_of_small_maintains_sort [in Selection]
contents_perm [in Multiset]
contents_insert_other [in Multiset]
contents_cons_inv [in Multiset]
contents_nil_inv [in Multiset]
count_insert_other [in BagPerm]

E

elements_relate' [in SearchTree]
elements_relate [in SearchTree]
elements_empty [in SearchTree]
elements_nodup_keys [in SearchTree]
elements_correct_inverse [in SearchTree]
elements_complete_inverse [in SearchTree]
elements_correct [in SearchTree]
elements_preserves_relation [in SearchTree]
elements_preserves_forall [in SearchTree]
elements_complete [in SearchTree]
elements_complete_broken [in SearchTree]
empty_relate [in Trie]
empty_is_trie [in Trie]
empty_tree_BST [in Redblack]
empty_relate' [in SearchTree]
empty_relate [in SearchTree]
empty_tree_BST [in SearchTree]
eqb_reflect [in Perm]
eqlistA_Eeq_eq [in Color]
Even2 [in ADT]

F

fast_elements_correct [in SearchTree]
fast_elements_eq_elements [in SearchTree]
fast_elements_tr_helper [in SearchTree]
filter_sortE [in Color]
fold_right_rev_left [in Color]
ForallT_less [in Redblack]
ForallT_greater [in Redblack]
ForallT_imp [in Redblack]
ForallT_insert [in SearchTree]
Forall_perm [in Perm]
FunTable.get_set_other [in ADT]
FunTable.get_set_same [in ADT]
FunTable.get_empty_default [in ADT]

G

geb_reflect [in Perm]
gtb_reflect [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 Trie]
insert_is_trie [in Trie]
insert_RB [in Redblack]
insert_BST [in Redblack]
insert_BST [in Redblack]
insert_relate' [in SearchTree]
insert_relate [in SearchTree]
insert_permute_equality_breaks [in SearchTree]
insert_same_equality_breaks [in SearchTree]
insert_shadow_equality [in SearchTree]
insert_BST [in SearchTree]
insert_sorted' [in Sort]
insert_perm [in Sort]
insert_sorted [in Sort]
insert_bag [in BagPerm]
insert_contents [in Multiset]
insP [in Redblack]
ins_red [in Redblack]
ins_RB [in Redblack]
ins_BST [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_leb_reflect [in Extract]
int_ltb_reflect [in Extract]
in_colors_of_1 [in Color]
in_map_of_list [in SearchTree]
in_fst [in SearchTree]

K

kvs_insert_elements [in SearchTree]
kvs_insert_split [in SearchTree]

L

leb_reflect [in Perm]
le_all__le_one [in Selection]
lia_example_3 [in Perm]
lia_example2 [in Perm]
lia_example1 [in Perm]
lia_example1 [in Perm]
ListETableAbs.bound_relate [in ADT]
ListETableAbs.elements_relate [in ADT]
ListETableAbs.empty_relate [in ADT]
ListETableAbs.empty_ok [in ADT]
ListETableAbs.insert_relate [in ADT]
ListETableAbs.lookup_relate [in ADT]
ListETableAbs.set_ok [in ADT]
ListQueue.deq_nonempty [in ADT]
ListQueue.deq_empty [in ADT]
ListQueue.is_empty_nonempty [in ADT]
ListQueue.is_empty_empty [in ADT]
ListQueue.peek_nonempty [in ADT]
ListQueue.peek_empty [in ADT]
ListsTable.get_set_other [in ADT]
ListsTable.get_set_same [in ADT]
ListsTable.get_empty_default [in ADT]
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]
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]
lookup_relate' [in SearchTree]
lookup_relate [in SearchTree]
lookup_insert_permute [in SearchTree]
lookup_insert_same [in SearchTree]
lookup_insert_shadow [in SearchTree]
lookup_insert_neq [in SearchTree]
lookup_insert_eq' [in SearchTree]
lookup_insert_eq [in SearchTree]
lookup_empty [in SearchTree]
lookup_insert_neq [in Extract]
lookup_insert_eq [in Extract]
lookup_empty [in Extract]
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

map_of_list_app [in SearchTree]
map_of_tree_prop [in SearchTree]
maybe_swap_correct [in Perm]
maybe_swap_perm [in Perm]
maybe_swap_idempotent [in Perm]
maybe_swap_idempotent [in Perm]
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]
not_in_map_of_list [in SearchTree]
nth_error_insert [in Sort]

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

RB_blacken_root [in Redblack]
RB_blacken_parent [in Redblack]
redblack_balanced [in Redblack]

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]
selection_sort_correct' [in Selection]
selection_sort_contents [in Selection]
selection_sort_is_correct [in Selection]
selection_sort_sorted [in Selection]
selection_sort_perm [in Selection]
select_terminates [in Color]
select_contents [in Selection]
select_in [in Selection]
select_smallest [in Selection]
select_fst_leq [in Selection]
select_rest_length [in Selection]
select_perm [in Selection]
selsort_sorted [in Selection]
selsort_perm [in Selection]
selsort'_is_correct [in Selection]
selsort'_sorted [in Selection]
selsort'_perm [in Selection]
Sin_domain [in Color]
Snot_in_empty [in Color]
Sorted_lt_key [in Color]
sorted_elements [in SearchTree]
sorted_app [in SearchTree]
sorted_sorted' [in Sort]
sorted_iff_sorted [in Selection]
sorted_merge [in Merge]
sorted_merge1 [in Merge]
sorted'_sorted [in Sort]
SortE_equivlistE_eqlistE [in Color]
sort_sorted' [in Sort]
sort_perm [in Sort]
sort_sorted [in Sort]
sort_specifications_equivalent [in BagPerm]
sort_bag [in BagPerm]
sort_specifications_equivalent [in Multiset]
sort_contents [in Multiset]
sort_int_correct [in Extract]
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]
subset_nodes_sub [in Color]

T

three_less_seven_2 [in Decide]
three_less_seven_1 [in Decide]
TreeETableEncapsulated.bound_set_other [in ADT]
TreeETableEncapsulated.bound_set_same [in ADT]
TreeETableEncapsulated.bound_empty [in ADT]
TreeETableEncapsulated.elements_correct [in ADT]
TreeETableEncapsulated.elements_complete [in ADT]
TreeETableEncapsulated.empty_ok [in ADT]
TreeETableEncapsulated.set_ok [in ADT]
TreeETableFullyEncapsulated.bound_set_other [in ADT]
TreeETableFullyEncapsulated.bound_set_same [in ADT]
TreeETableFullyEncapsulated.bound_empty [in ADT]
TreeETableFullyEncapsulated.elements_correct [in ADT]
TreeETableFullyEncapsulated.elements_complete [in ADT]
TreeETableFullyEncapsulated.empty_ok [in ADT]
TreeETableFullyEncapsulated.set_ok [in ADT]
TreeETableSubset.bound_set_other [in ADT]
TreeETableSubset.bound_set_same [in ADT]
TreeETableSubset.bound_empty [in ADT]
TreeETableSubset.elements_correct [in ADT]
TreeETableSubset.elements_complete [in ADT]
TreeETableSubset.get_set_other [in ADT]
TreeETableSubset.get_set_same [in ADT]
TreeETableSubset.get_empty_default [in ADT]
TreeETable_first_attempt.elements_correct [in ADT]
TreeETable_first_attempt.elements_complete [in ADT]
TreeETable.bound_set_other [in ADT]
TreeETable.bound_set_same [in ADT]
TreeETable.bound_empty [in ADT]
TreeETable.elements_correct [in ADT]
TreeETable.elements_complete [in ADT]
TreeETable.empty_ok [in ADT]
TreeETable.set_ok [in ADT]
TreeTable.get_set_other [in ADT]
TreeTable.get_set_same [in ADT]
TreeTable.get_empty_default [in ADT]
truncated_subtraction [in Perm]
TwoListQueueAbs.deq_relate [in ADT]
TwoListQueueAbs.empty_relate [in ADT]
TwoListQueueAbs.enq_relate [in ADT]
TwoListQueueAbs.peek_relate [in ADT]
t_update_permute [in Maps]
t_update_same [in Maps]
t_update_shadow [in Maps]
t_update_neq [in Maps]
t_update_eq [in Maps]
t_apply_empty [in Maps]

U

union_update_left [in SearchTree]
union_update_right [in SearchTree]
union_both [in SearchTree]
union_right [in SearchTree]
union_left [in SearchTree]
union_swap [in Multiset]
union_comm [in Multiset]
union_assoc [in Multiset]
update_permute [in Maps]
update_same [in Maps]
update_shadow [in Maps]
update_neq [in Maps]
update_eq [in Maps]

V

vector_app_correct [in ADT]
vector_cons_correct [in ADT]

Z

Z_geb_reflect [in Extract]
Z_gtb_reflect [in Extract]
Z_leb_reflect [in Extract]
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]
BST_T [in SearchTree]
BST_E [in SearchTree]

E

E [in Redblack]
E [in SearchTree]
E [in Extract]

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]

L

Leaf [in Trie]
List_Priqueue.Abs_intro [in Priqueue]

N

NearlyRB_b [in Redblack]
NearlyRB_r [in Redblack]
Node [in Trie]

R

RB_b [in Redblack]
RB_r [in Redblack]
RB_leaf [in Redblack]
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]
SigSandbox.exist [in ADT]
SigSandbox.ex_intro [in ADT]
sorted_cons [in Sort]
sorted_1 [in Sort]
sorted_nil [in Sort]
sorted_cons [in Selection]
sorted_1 [in Selection]
sorted_nil [in Selection]
sorted_cons [in Extract]
sorted_1 [in Extract]
sorted_nil [in Extract]
ST_T [in Redblack]
ST_E [in Redblack]

T

T [in Redblack]
T [in SearchTree]
T [in Extract]

Axiom Index

A

Abs [in Extract]
Abs_inj [in Extract]

E

ETableAbs.Abs [in ADT]
ETableAbs.bound [in ADT]
ETableAbs.bound_relate [in ADT]
ETableAbs.default [in ADT]
ETableAbs.elements [in ADT]
ETableAbs.elements_relate [in ADT]
ETableAbs.empty [in ADT]
ETableAbs.empty_relate [in ADT]
ETableAbs.empty_ok [in ADT]
ETableAbs.get [in ADT]
ETableAbs.insert_relate [in ADT]
ETableAbs.lookup_relate [in ADT]
ETableAbs.rep_ok [in ADT]
ETableAbs.set [in ADT]
ETableAbs.set_ok [in ADT]
ETableAbs.table [in ADT]
ETableAbs.V [in ADT]
ETableSubset.bound [in ADT]
ETableSubset.bound_set_other [in ADT]
ETableSubset.bound_set_same [in ADT]
ETableSubset.bound_empty [in ADT]
ETableSubset.elements [in ADT]
ETableSubset.elements_correct [in ADT]
ETableSubset.elements_complete [in ADT]
ETable_first_attempt.elements_correct [in ADT]
ETable_first_attempt.elements_complete [in ADT]
ETable_first_attempt.elements [in ADT]
ETable_first_attempt.bound [in ADT]
ETable.bound [in ADT]
ETable.bound_set_other [in ADT]
ETable.bound_set_same [in ADT]
ETable.bound_empty [in ADT]
ETable.elements [in ADT]
ETable.elements_correct [in ADT]
ETable.elements_complete [in ADT]
ETable.empty_ok [in ADT]
ETable.rep_ok [in ADT]
ETable.set_ok [in ADT]

I

int [in Extract]

L

leb [in Extract]
leb_le [in Extract]
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]

Q

QueueAbs.Abs [in ADT]
QueueAbs.deq [in ADT]
QueueAbs.deq_relate [in ADT]
QueueAbs.empty [in ADT]
QueueAbs.empty_relate [in ADT]
QueueAbs.enq [in ADT]
QueueAbs.enq_relate [in ADT]
QueueAbs.is_empty [in ADT]
QueueAbs.peek [in ADT]
QueueAbs.peek_relate [in ADT]
QueueAbs.queue [in ADT]
QueueAbs.V [in ADT]
Queue.deq [in ADT]
Queue.deq_nonempty [in ADT]
Queue.deq_empty [in ADT]
Queue.empty [in ADT]
Queue.enq [in ADT]
Queue.is_empty_nonempty [in ADT]
Queue.is_empty_empty [in ADT]
Queue.is_empty [in ADT]
Queue.peek [in ADT]
Queue.peek_nonempty [in ADT]
Queue.peek_empty [in ADT]
Queue.queue [in ADT]
Queue.V [in ADT]

S

ScratchPad2.lt_dec_axiom_2 [in Decide]
ScratchPad2.lt_dec_axiom_1 [in Decide]
SimpleTable.default [in ADT]
SimpleTable.key [in ADT]
SimpleTable.table [in ADT]
SimpleTable.V [in ADT]

T

Table.default [in ADT]
Table.empty [in ADT]
Table.get [in ADT]
Table.get_set_other [in ADT]
Table.get_set_same [in ADT]
Table.get_empty_default [in ADT]
Table.set [in ADT]
Table.table [in ADT]
Table.V [in ADT]

V

ValType.default [in ADT]
ValType.V [in ADT]

Inductive Index

B

BinomQueue.priqueue_elems [in Binom]
BinomQueue.tree [in Binom]
BinomQueue.tree_elems [in Binom]
BST [in Redblack]
BST [in SearchTree]

C

color [in Redblack]

I

Integers.comparison [in Trie]
Integers.positive [in Trie]
Integers.Z [in Trie]

L

List_Priqueue.Abs' [in Priqueue]

N

NearlyRB [in Redblack]

R

RB [in Redblack]

S

ScratchPad.sumbool [in Decide]
ScratchPad2.sorted [in Decide]
SigSandbox.ex [in ADT]
SigSandbox.sig [in ADT]
sorted [in Sort]
sorted [in Selection]
sorted [in Extract]

T

tree [in Redblack]
tree [in SearchTree]
tree [in Extract]
trie [in Trie]

Definition Index

A

Abs [in Trie]
Abs [in SearchTree]
abstract [in Trie]
Abs_three_ten [in Trie]
Abs' [in SearchTree]
add_edge [in Color]
adj [in Color]
a_vector [in ADT]

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.priqueue_elems_sind [in Binom]
BinomQueue.priqueue_elems_rec [in Binom]
BinomQueue.priqueue_elems_ind [in Binom]
BinomQueue.priqueue_elems_rect [in Binom]
BinomQueue.priq' [in Binom]
BinomQueue.smash [in Binom]
BinomQueue.tree_elems_sind [in Binom]
BinomQueue.tree_elems_ind [in Binom]
BinomQueue.tree_sind [in Binom]
BinomQueue.tree_rec [in Binom]
BinomQueue.tree_ind [in Binom]
BinomQueue.tree_rect [in Binom]
BinomQueue.unzip [in Binom]
bound [in SearchTree]
BST_sind [in Redblack]
BST_ind [in Redblack]
BST_sind [in SearchTree]
BST_ind [in SearchTree]
butterfly [in Perm]

C

color [in Color]
coloring [in Color]
coloring_ok [in Color]
colors_of [in Color]
color_sind [in Redblack]
color_rec [in Redblack]
color_ind [in Redblack]
color_rect [in Redblack]
color1 [in Color]
contents [in Multiset]
count [in BagPerm]

D

disjoint [in SearchTree]
domain_example_map [in Color]

E

elements [in Redblack]
elements [in SearchTree]
elements [in Extract]
elements_aux [in Redblack]
elements_correct_spec [in SearchTree]
elements_complete_spec [in SearchTree]
elements_complete_broken_spec [in SearchTree]
elements_ex [in SearchTree]
elements_aux [in Extract]
empty [in Trie]
empty [in Multiset]
empty [in Maps]
empty_tree [in Redblack]
empty_tree [in SearchTree]
empty_map [in ADT]
empty_tree [in Extract]
equivlistA_example [in Color]
ETableAbs.key [in ADT]
even_nat [in ADT]
Even2' [in ADT]
examplemap [in Maps]
example_map [in Color]
exposed_trees_ex [in ADT]
extra_fuel [in Selection]
ex_tree [in SearchTree]

F

FastEnough.collisions [in Trie]
FastEnough.collisions_pi [in Trie]
FastEnough.loop [in Trie]
fast_elements [in SearchTree]
fast_elements_tr [in SearchTree]
find [in SearchTree]
first_le_second [in Perm]
ForallT [in Redblack]
ForallT [in SearchTree]
FunTableExamples.ex1 [in ADT]
FunTableExamples.ex2 [in ADT]
FunTableExamples.ex3 [in ADT]
FunTable.default [in ADT]
FunTable.empty [in ADT]
FunTable.get [in ADT]
FunTable.key [in ADT]
FunTable.set [in ADT]
FunTable.table [in ADT]
FunTable.V [in ADT]

G

G [in Color]
geb [in Perm]
graph [in Color]
gtb [in Perm]

H

height [in Redblack]

I

InA_example [in Color]
ins [in Trie]
ins [in Redblack]
ins [in Extract]
insert [in Trie]
insert [in Redblack]
insert [in SearchTree]
insert [in Sort]
insert [in Extract]
insZ [in Extract]
ins_int [in Extract]
Integers.add [in Trie]
Integers.addc [in Trie]
Integers.compare [in Trie]
Integers.comparison_sind [in Trie]
Integers.comparison_rec [in Trie]
Integers.comparison_ind [in Trie]
Integers.comparison_rect [in Trie]
Integers.positive_sind [in Trie]
Integers.positive_rec [in Trie]
Integers.positive_ind [in Trie]
Integers.positive_rect [in Trie]
Integers.positive2nat [in Trie]
Integers.print_in_binary [in Trie]
Integers.succ [in Trie]
Integers.ten [in Trie]
Integers.Z_sind [in Trie]
Integers.Z_rec [in Trie]
Integers.Z_ind [in Trie]
Integers.Z_rect [in Trie]
in_4_pi [in Decide]
is_trie [in Trie]
is_BST_ex [in SearchTree]
is_a_sorting_algorithm [in Sort]
is_a_sorting_algorithm' [in BagPerm]
is_a_sorting_algorithm [in Selection]
is_a_sorting_algorithm' [in Multiset]

K

key [in Redblack]
key [in SearchTree]
key [in Extract]
kvs_insert [in SearchTree]

L

le_all [in Selection]
ListETableAbs.Abs [in ADT]
ListETableAbs.bound [in ADT]
ListETableAbs.default [in ADT]
ListETableAbs.elements [in ADT]
ListETableAbs.empty [in ADT]
ListETableAbs.get [in ADT]
ListETableAbs.key [in ADT]
ListETableAbs.rep_ok [in ADT]
ListETableAbs.set [in ADT]
ListETableAbs.table [in ADT]
ListETableAbs.V [in ADT]
ListQueue.deq [in ADT]
ListQueue.empty [in ADT]
ListQueue.enq [in ADT]
ListQueue.is_empty [in ADT]
ListQueue.peek [in ADT]
ListQueue.queue [in ADT]
ListQueue.V [in ADT]
ListsTable.default [in ADT]
ListsTable.empty [in ADT]
ListsTable.get [in ADT]
ListsTable.key [in ADT]
ListsTable.set [in ADT]
ListsTable.table [in ADT]
ListsTable.V [in ADT]
List_Priqueue.Abs [in Priqueue]
List_Priqueue.Abs'_sind [in Priqueue]
List_Priqueue.Abs'_ind [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]
list_keys [in SearchTree]
list_nat_in [in Decide]
list_nat_eq_dec [in Decide]
list_of_vector [in ADT]
list_ind2 [in Merge]
list_ind2_principle [in Merge]
look [in Trie]
lookup [in Trie]
lookup [in Redblack]
lookup [in SearchTree]
lookup [in Extract]
low_deg [in Color]

M

make_black [in Redblack]
manual_grade_for_successor_of_Z_constant_time [in Trie]
manual_grade_for_redblack_bound [in Redblack]
manual_grade_for_bound_correct [in SearchTree]
manual_grade_for_permutations_vs_multiset [in BagPerm]
manual_grade_for_ListsETable [in ADT]
manual_grade_for_TreeTableModel [in ADT]
map_of_tree [in SearchTree]
map_bound [in SearchTree]
map_of_list [in SearchTree]
map_find [in ADT]
map_update [in ADT]
maybe_swap_321 [in Perm]
maybe_swap_123 [in Perm]
maybe_swap [in Perm]
Mdomain [in Color]
merge [in Merge]
mindepth [in Redblack]
mk_graph [in Color]
multiset [in Multiset]

N

nat2pos [in Trie]
NearlyRB_sind [in Redblack]
NearlyRB_ind [in Redblack]
NicelyEncapsulatedExample.ex1 [in ADT]
NicelyEncapsulatedExample.ex2 [in ADT]
node [in Color]
nodemap [in Color]
nodes [in Color]
nodeset [in Color]
NotBst.not_bst_lookup_wrong [in SearchTree]
NotBst.t [in SearchTree]
not_BST_ex [in SearchTree]
not_a_permutation [in Perm]
no_selfloop [in Color]

O

out_of_fuel [in Selection]
OverlyEncapsulatedExample.ex1 [in ADT]

P

pairs_example [in Selection]
palette [in Color]
partial_map [in Maps]
permut_example [in Perm]
plus_two [in ADT]
plus_two [in ADT]
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]
RB_sind [in Redblack]
RB_ind [in Redblack]
reflect_example2 [in Perm]
reflect_example1' [in Perm]
reflect_example1 [in Perm]
remove_node [in Color]

S

same_mod_10 [in Color]
ScratchPad.is_3_less_7 [in Decide]
ScratchPad.lt_dec' [in Decide]
ScratchPad.lt_dec [in Decide]
ScratchPad.sumbool_sind [in Decide]
ScratchPad.sumbool_rec [in Decide]
ScratchPad.sumbool_ind [in Decide]
ScratchPad.sumbool_rect [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]
ScratchPad2.sorted_sind [in Decide]
ScratchPad2.sorted_ind [in Decide]
select [in Selection]
selection_sort [in Selection]
selsort [in Selection]
selsort [in Selection]
selsort'_example [in Selection]
SigSandbox.ex_sind [in ADT]
SigSandbox.ex_ind [in ADT]
SigSandbox.proj1_ex [in ADT]
SigSandbox.proj1_sig [in ADT]
SigSandbox.proj2_sig [in ADT]
SigSandbox.sig_sind [in ADT]
SigSandbox.sig_rec [in ADT]
SigSandbox.sig_ind [in ADT]
SigSandbox.sig_rect [in ADT]
SimpleStringTable1.default [in ADT]
SimpleStringTable1.key [in ADT]
SimpleStringTable1.table [in ADT]
SimpleStringTable1.V [in ADT]
SimpleStringTable2.default [in ADT]
SimpleStringTable2.key [in ADT]
SimpleStringTable2.table [in ADT]
SimpleStringTable2.V [in ADT]
SimpleStringTable3.default [in ADT]
SimpleStringTable3.key [in ADT]
SimpleStringTable3.table [in ADT]
SimpleStringTable3.V [in ADT]
singleton [in Multiset]
sort [in Sort]
sort [in Extract]
sorted_sind [in Sort]
sorted_ind [in Sort]
sorted_sind [in Selection]
sorted_ind [in Selection]
sorted_sind [in Extract]
sorted_ind [in Extract]
sorted' [in Sort]
sorted'' [in Sort]
sortZ [in Extract]
sort_pi [in Sort]
sort_pi [in Selection]
sort_pi_same_contents [in Multiset]
sort_int [in Extract]
split [in Merge]
StringListsTableExamples.ex1 [in ADT]
StringListsTableExamples.ex2 [in ADT]
StringListsTableExamples.ex3 [in ADT]
StringTreeETableExample.ex1 [in ADT]
StringVal.default [in ADT]
StringVal.V [in ADT]
subset_nodes [in Color]

T

Table.key [in ADT]
Tests.bst_ex₄ [in SearchTree]
Tests.bst_ex₃ [in SearchTree]
Tests.bst_ex₂ [in SearchTree]
Tests.bst_ex₁ [in SearchTree]
three_ten [in Trie]
total_map [in Maps]
TreeETableEncapsulated.bound [in ADT]
TreeETableEncapsulated.elements [in ADT]
TreeETableEncapsulated.rep_ok [in ADT]
TreeETableFullyEncapsulated.bound [in ADT]
TreeETableFullyEncapsulated.elements [in ADT]
TreeETableFullyEncapsulated.rep_ok [in ADT]
TreeETableSubset.bound [in ADT]
TreeETableSubset.default [in ADT]
TreeETableSubset.elements [in ADT]
TreeETableSubset.empty [in ADT]
TreeETableSubset.get [in ADT]
TreeETableSubset.key [in ADT]
TreeETableSubset.set [in ADT]
TreeETableSubset.table [in ADT]
TreeETableSubset.V [in ADT]
TreeETable_first_attempt.elements [in ADT]
TreeETable_first_attempt.bound [in ADT]
TreeETable.bound [in ADT]
TreeETable.elements [in ADT]
TreeETable.rep_ok [in ADT]
TreeTable.default [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]
tree_sind [in Redblack]
tree_rec [in Redblack]
tree_ind [in Redblack]
tree_rect [in Redblack]
tree_sind [in SearchTree]
tree_rec [in SearchTree]
tree_ind [in SearchTree]
tree_rect [in SearchTree]
tree_sind [in Extract]
tree_rec [in Extract]
tree_ind [in Extract]
tree_rect [in Extract]
trie_table [in Trie]
trie_sind [in Trie]
trie_rec [in Trie]
trie_ind [in Trie]
trie_rect [in Trie]
two [in ADT]
two [in ADT]
TwoListQueueAbs.Abs [in ADT]
TwoListQueueAbs.deq [in ADT]
TwoListQueueAbs.empty [in ADT]
TwoListQueueAbs.enq [in ADT]
TwoListQueueAbs.is_empty [in ADT]
TwoListQueueAbs.peek [in ADT]
TwoListQueueAbs.queue [in ADT]
TwoListQueueAbs.V [in ADT]
two' [in ADT]
t_update [in Maps]
t_empty [in Maps]

U

uncurry [in SearchTree]
undirected [in Color]
union [in SearchTree]
union [in Multiset]
Unnamed_thm [in Trie]
Unnamed_thm0 [in Color]
Unnamed_thm [in Color]
Unnamed_thm [in Decide]
update [in Maps]
update_example4 [in Maps]
update_example3 [in Maps]
update_example2 [in Maps]
update_example1 [in Maps]

V

value [in Multiset]
vector [in ADT]
vector_app [in ADT]
vector_cons [in ADT]
VerySlow.collisions [in Trie]
VerySlow.collisions_pi [in Trie]
VerySlow.loop [in Trie]

Global Index

J

X

Y

_

(997 entries)

Notation Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(7 entries)

Module Index

A

C

D

G

H

J

K

U

X

Y

Z

_

other

(55 entries)

Library Index

F

G

H

I

J

K

L

N

O

Q

U

V

W

X

Y

Z

_

other

(17 entries)

Lemma Index

D

H

J

O

Q

W

X

Y

_

other

(330 entries)

Constructor Index

A

C

D

F

G

H

J

K

M

O

P

Q

U

V

W

X

Y

Z

_

other

(49 entries)

Axiom Index

B

C

D

F

G

H

J

K

M

N

O

R

U

W

X

Y

Z

_

other

(105 entries)

Inductive Index

A

D

E

F

G

H

J

K

M

O

P

Q

U

V

W

X

Y

Z

_

other

(23 entries)

Definition Index

J

Q

W

X

Y

Z

_

other

(411 entries)

This page has been generated by coqdoc