| 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 | (77 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 | (1 entry) |
| 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 | (21 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 | (7 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 | (4 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 | (44 entries) |
Global Index
A
atoi [definition, in Hbt.Implementation.hbt]B
binary_tree_induction [definition, in Hbt.Implementation.hbt]binary_tree [inductive, in Hbt.Implementation.hbt]
bt_to_list [definition, in Hbt.Implementation.hbt]
D
differ_by_one [definition, in Hbt.Implementation.hbt]E
equal_hbt [definition, in Hbt.Implementation.hbt]equal_lists [definition, in Hbt.Implementation.hbt]
F
fold_unfold_insert_t_helper [lemma, in Hbt.Implementation.hbt]fold_unfold_insert_bt_helper_node [lemma, in Hbt.Implementation.hbt]
fold_unfold_insert_bt_helper_leaf [lemma, in Hbt.Implementation.hbt]
fold_unfold_insert_hbt_helper [lemma, in Hbt.Implementation.hbt]
fold_unfold_occurs_t [lemma, in Hbt.Implementation.hbt]
fold_unfold_occurs_bt_node [lemma, in Hbt.Implementation.hbt]
fold_unfold_occurs_bt_leaf [lemma, in Hbt.Implementation.hbt]
fold_unfold_occurs_hbt [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_t [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_bt_node [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_bt_leaf [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_hbt [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_t [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_bt_node [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_bt_leaf [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_hbt [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_t [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_bt_node [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_bt_leaf [lemma, in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_hbt [lemma, in Hbt.Implementation.hbt]
H
hbt [library]hbt_1 [definition, in Hbt.Implementation.hbt]
hbt_empty [definition, in Hbt.Implementation.hbt]
hbt_to_list [definition, in Hbt.Implementation.hbt]
heightened_binary_tree_mutual_induction [definition, in Hbt.Implementation.hbt]
heightened_binary_tree_induction [definition, in Hbt.Implementation.hbt]
heightened_binary_tree [inductive, in Hbt.Implementation.hbt]
HNode [constructor, in Hbt.Implementation.hbt]
I
insert_hbt [definition, in Hbt.Implementation.hbt]insert_t_helper [definition, in Hbt.Implementation.hbt]
insert_bt_helper [definition, in Hbt.Implementation.hbt]
insert_hbt_helper [definition, in Hbt.Implementation.hbt]
insert_list [definition, in Hbt.Implementation.hbt]
iota [definition, in Hbt.Implementation.hbt]
is_ordered_hbt [definition, in Hbt.Implementation.hbt]
is_balanced_hbt [definition, in Hbt.Implementation.hbt]
is_sound_hbt [definition, in Hbt.Implementation.hbt]
L
Leaf [constructor, in Hbt.Implementation.hbt]N
Node [constructor, in Hbt.Implementation.hbt]O
occurs_t [definition, in Hbt.Implementation.hbt]occurs_bt [definition, in Hbt.Implementation.hbt]
occurs_hbt [definition, in Hbt.Implementation.hbt]
P
project_height_t [definition, in Hbt.Implementation.hbt]project_height_bt [definition, in Hbt.Implementation.hbt]
project_bt_hbt [definition, in Hbt.Implementation.hbt]
project_height_hbt [definition, in Hbt.Implementation.hbt]
R
rotate_left_hbt [definition, in Hbt.Implementation.hbt]rotate_left_bt [definition, in Hbt.Implementation.hbt]
rotate_right_hbt [definition, in Hbt.Implementation.hbt]
rotate_right_bt [definition, in Hbt.Implementation.hbt]
T
TError [constructor, in Hbt.Implementation.hbt]test_insert_hbt [definition, in Hbt.Implementation.hbt]
TNone [constructor, in Hbt.Implementation.hbt]
traverse [definition, in Hbt.Implementation.hbt]
traverse_to_check_ordered_t [definition, in Hbt.Implementation.hbt]
traverse_to_check_ordered_bt [definition, in Hbt.Implementation.hbt]
traverse_to_check_ordered_hbt [definition, in Hbt.Implementation.hbt]
traverse_to_check_balanced_t [definition, in Hbt.Implementation.hbt]
traverse_to_check_balanced_bt [definition, in Hbt.Implementation.hbt]
traverse_to_check_balanced_hbt [definition, in Hbt.Implementation.hbt]
traverse_to_check_soundness_t [definition, in Hbt.Implementation.hbt]
traverse_to_check_soundness_bt [definition, in Hbt.Implementation.hbt]
traverse_to_check_soundness_hbt [definition, in Hbt.Implementation.hbt]
Triple [constructor, in Hbt.Implementation.hbt]
triple [inductive, in Hbt.Implementation.hbt]
triple_option [inductive, in Hbt.Implementation.hbt]
triple_induction [definition, in Hbt.Implementation.hbt]
TSome [constructor, in Hbt.Implementation.hbt]
tsome_x_equal_tsome_y [lemma, in Hbt.Implementation.hbt]
t_to_list [definition, in Hbt.Implementation.hbt]
Library Index
H
hbtLemma Index
F
fold_unfold_insert_t_helper [in Hbt.Implementation.hbt]fold_unfold_insert_bt_helper_node [in Hbt.Implementation.hbt]
fold_unfold_insert_bt_helper_leaf [in Hbt.Implementation.hbt]
fold_unfold_insert_hbt_helper [in Hbt.Implementation.hbt]
fold_unfold_occurs_t [in Hbt.Implementation.hbt]
fold_unfold_occurs_bt_node [in Hbt.Implementation.hbt]
fold_unfold_occurs_bt_leaf [in Hbt.Implementation.hbt]
fold_unfold_occurs_hbt [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_t [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_bt_node [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_bt_leaf [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_ordered_hbt [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_t [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_bt_node [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_bt_leaf [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_balanced_hbt [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_t [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_bt_node [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_bt_leaf [in Hbt.Implementation.hbt]
fold_unfold_traverse_to_check_soundness_hbt [in Hbt.Implementation.hbt]
T
tsome_x_equal_tsome_y [in Hbt.Implementation.hbt]Constructor Index
H
HNode [in Hbt.Implementation.hbt]L
Leaf [in Hbt.Implementation.hbt]N
Node [in Hbt.Implementation.hbt]T
TError [in Hbt.Implementation.hbt]TNone [in Hbt.Implementation.hbt]
Triple [in Hbt.Implementation.hbt]
TSome [in Hbt.Implementation.hbt]
Inductive Index
B
binary_tree [in Hbt.Implementation.hbt]H
heightened_binary_tree [in Hbt.Implementation.hbt]T
triple [in Hbt.Implementation.hbt]triple_option [in Hbt.Implementation.hbt]
Definition Index
A
atoi [in Hbt.Implementation.hbt]B
binary_tree_induction [in Hbt.Implementation.hbt]bt_to_list [in Hbt.Implementation.hbt]
D
differ_by_one [in Hbt.Implementation.hbt]E
equal_hbt [in Hbt.Implementation.hbt]equal_lists [in Hbt.Implementation.hbt]
H
hbt_1 [in Hbt.Implementation.hbt]hbt_empty [in Hbt.Implementation.hbt]
hbt_to_list [in Hbt.Implementation.hbt]
heightened_binary_tree_mutual_induction [in Hbt.Implementation.hbt]
heightened_binary_tree_induction [in Hbt.Implementation.hbt]
I
insert_hbt [in Hbt.Implementation.hbt]insert_t_helper [in Hbt.Implementation.hbt]
insert_bt_helper [in Hbt.Implementation.hbt]
insert_hbt_helper [in Hbt.Implementation.hbt]
insert_list [in Hbt.Implementation.hbt]
iota [in Hbt.Implementation.hbt]
is_ordered_hbt [in Hbt.Implementation.hbt]
is_balanced_hbt [in Hbt.Implementation.hbt]
is_sound_hbt [in Hbt.Implementation.hbt]
O
occurs_t [in Hbt.Implementation.hbt]occurs_bt [in Hbt.Implementation.hbt]
occurs_hbt [in Hbt.Implementation.hbt]
P
project_height_t [in Hbt.Implementation.hbt]project_height_bt [in Hbt.Implementation.hbt]
project_bt_hbt [in Hbt.Implementation.hbt]
project_height_hbt [in Hbt.Implementation.hbt]
R
rotate_left_hbt [in Hbt.Implementation.hbt]rotate_left_bt [in Hbt.Implementation.hbt]
rotate_right_hbt [in Hbt.Implementation.hbt]
rotate_right_bt [in Hbt.Implementation.hbt]
T
test_insert_hbt [in Hbt.Implementation.hbt]traverse [in Hbt.Implementation.hbt]
traverse_to_check_ordered_t [in Hbt.Implementation.hbt]
traverse_to_check_ordered_bt [in Hbt.Implementation.hbt]
traverse_to_check_ordered_hbt [in Hbt.Implementation.hbt]
traverse_to_check_balanced_t [in Hbt.Implementation.hbt]
traverse_to_check_balanced_bt [in Hbt.Implementation.hbt]
traverse_to_check_balanced_hbt [in Hbt.Implementation.hbt]
traverse_to_check_soundness_t [in Hbt.Implementation.hbt]
traverse_to_check_soundness_bt [in Hbt.Implementation.hbt]
traverse_to_check_soundness_hbt [in Hbt.Implementation.hbt]
triple_induction [in Hbt.Implementation.hbt]
t_to_list [in Hbt.Implementation.hbt]
| 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 | (77 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 | (1 entry) |
| 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 | (21 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 | (7 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 | (4 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 | (44 entries) |
This page has been generated by coqdoc