| 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 | (2019 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 | (15 entries) |
| Binder 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 | (1214 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 | (16 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 | (20 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 | (249 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 | (131 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 | (39 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 | (335 entries) |
Global Index
A
A [constructor, in Intro]addn_preserves_sortedness [lemma, in Sorting2]
add1_preserves_sortedness [lemma, in Sorting2]
add2_preserves_sortedness [lemma, in Sorting2]
aeval [definition, in Expressions]
aexp [inductive, in Expressions]
AExp [module, in Expressions]
AExp.aeval [definition, in Expressions]
AExp.aexp [inductive, in Expressions]
AExp.AMinus [constructor, in Expressions]
AExp.AMult [constructor, in Expressions]
AExp.ANum [constructor, in Expressions]
AExp.APlus [constructor, in Expressions]
AExp.BAnd [constructor, in Expressions]
AExp.BEq [constructor, in Expressions]
AExp.beval [definition, in Expressions]
AExp.bexp [inductive, in Expressions]
AExp.BFalse [constructor, in Expressions]
AExp.BLe [constructor, in Expressions]
AExp.BNot [constructor, in Expressions]
AExp.BTrue [constructor, in Expressions]
AExp.optimize_0plus [definition, in Expressions]
AId [constructor, in Expressions]
Ala [constructor, in Lists]
All [inductive, in Indprop2]
allb [definition, in Structures]
All_In [lemma, in Indprop2]
All_cons [constructor, in Indprop2]
All_nil [constructor, in Indprop2]
All_nth [lemma, in Sorting2]
All_perm [lemma, in Sorting2]
all3_spec [lemma, in Induction]
al:103 [binder, in Sorting2]
al:26 [binder, in Sorting2]
al:67 [binder, in Sorting2]
al:71 [binder, in Sorting2]
al:77 [binder, in Sorting2]
al:98 [binder, in Sorting2]
al:99 [binder, in Sorting2]
AMinus [constructor, in Expressions]
AMult [constructor, in Expressions]
andb [definition, in Intro]
andb_false_r [lemma, in Induction]
andb_true_iff [lemma, in Cases]
andb_true_elim2 [lemma, in Cases]
andb_commutative'' [lemma, in Cases]
andb_commutative' [lemma, in Cases]
andb_commutative [lemma, in Cases]
andb3_exchange [lemma, in Cases]
and_PQ [lemma, in Propositions]
and_example' [definition, in Propositions]
and_example [definition, in Propositions]
and_intro_sloppy [lemma, in Propositions]
and_intro_braces [lemma, in Propositions]
and_intro [lemma, in Propositions]
and_option [definition, in Structures]
and_then [definition, in Structures]
and_example2'' [lemma, in Cases]
and_example2' [lemma, in Cases]
and_example2 [lemma, in Cases]
and_assoc [lemma, in Cases]
and_commut [lemma, in Cases]
ANum [constructor, in Expressions]
APlus [constructor, in Expressions]
app [definition, in Structures]
apply_iff_example [lemma, in Cases]
app_length [lemma, in Induction]
app_nil_r [lemma, in Induction]
app_assoc [lemma, in Induction]
Arg [constructor, in Lists]
argmin [definition, in Structures]
argmin [definition, in Types]
argmin3 [definition, in Structures]
argmin3 [definition, in Cases]
argmin3 [definition, in Types]
argmin3_leb [lemma, in Indprop2]
argmin3_min [lemma, in Indprop2]
argmin3_min3 [lemma, in Cases]
argmin3_min3_eqs [lemma, in Cases]
argmin3' [definition, in Types]
Asn [constructor, in Lists]
Asp [constructor, in Lists]
assumed_A [lemma, in Propositions]
a1:12 [binder, in Expressions]
a1:14 [binder, in Expressions]
a1:38 [binder, in Expressions]
a1:4 [binder, in Expressions]
a1:40 [binder, in Expressions]
a1:42 [binder, in Expressions]
a1:46 [binder, in Expressions]
a1:48 [binder, in Expressions]
a1:6 [binder, in Expressions]
a1:62 [binder, in Expressions]
a1:64 [binder, in Expressions]
a1:66 [binder, in Expressions]
a1:68 [binder, in Expressions]
a1:8 [binder, in Expressions]
a2:13 [binder, in Expressions]
a2:15 [binder, in Expressions]
a2:39 [binder, in Expressions]
a2:41 [binder, in Expressions]
a2:43 [binder, in Expressions]
a2:47 [binder, in Expressions]
a2:49 [binder, in Expressions]
a2:5 [binder, in Expressions]
a2:63 [binder, in Expressions]
a2:65 [binder, in Expressions]
a2:67 [binder, in Expressions]
a2:69 [binder, in Expressions]
a2:7 [binder, in Expressions]
a2:9 [binder, in Expressions]
A:1 [binder, in Sorting2]
A:100 [binder, in Sorting2]
a:105 [binder, in Sorting2]
a:117 [binder, in Cases]
a:120 [binder, in Cases]
A:129 [binder, in Structures]
A:135 [binder, in Structures]
A:146 [binder, in Cases]
A:154 [binder, in Cases]
A:16 [binder, in Propositions]
A:16 [binder, in Sorting2]
A:162 [binder, in Cases]
a:17 [binder, in Indprop2]
A:18 [binder, in Sorting2]
a:19 [binder, in Expressions]
A:21 [binder, in Sorting2]
A:22 [binder, in Propositions]
A:24 [binder, in Propositions]
A:24 [binder, in Sorting2]
a:24 [binder, in Expressions]
A:26 [binder, in Propositions]
A:28 [binder, in Sorting2]
a:29 [binder, in Sorting2]
A:30 [binder, in Propositions]
A:32 [binder, in Propositions]
A:34 [binder, in Sorting2]
A:36 [binder, in Propositions]
A:37 [binder, in Propositions]
A:38 [binder, in Sorting2]
A:40 [binder, in Indprop2]
A:42 [binder, in Sorting2]
a:44 [binder, in Induction]
A:45 [binder, in Indprop2]
A:47 [binder, in Induction]
A:5 [binder, in Induction2]
A:51 [binder, in Indprop2]
a:54 [binder, in Expressions]
A:62 [binder, in Indprop2]
a:63 [binder, in Propositions]
A:67 [binder, in Indprop2]
A:67 [binder, in Induction]
A:7 [binder, in Propositions]
A:73 [binder, in Indprop2]
a:73 [binder, in Propositions]
a:76 [binder, in Indprop2]
a:79 [binder, in Propositions]
A:83 [binder, in Indprop2]
a:93 [binder, in Sorting2]
B
bad_function_breaks_sortedness [lemma, in Sorting2]bad_function [definition, in Sorting2]
BAnd [constructor, in Expressions]
bar [definition, in Cases]
base [inductive, in Intro]
bb_node [constructor, in Indprop]
bb_empty [constructor, in Indprop]
BEq [constructor, in Expressions]
best:65 [binder, in Higherorder]
best:68 [binder, in Higherorder]
best:75 [binder, in Higherorder]
best:80 [binder, in Higherorder]
best:85 [binder, in Higherorder]
beval [definition, in Expressions]
bexp [inductive, in Expressions]
BFalse [constructor, in Expressions]
bge [definition, in Expressions]
bgt [definition, in Expressions]
bin [inductive, in Recursion]
bin_nat_bin [lemma, in Induction]
bin_to_nat [definition, in Induction]
black [constructor, in Types]
BLe [constructor, in Expressions]
blt [definition, in Expressions]
blue [constructor, in Types]
bl:27 [binder, in Sorting2]
bne [definition, in Expressions]
BNot [constructor, in Expressions]
bool [inductive, in Intro]
bor [definition, in Expressions]
BSTSets [module, in Sets]
BSTSets.empty_natset [definition, in Sets]
BSTSets.manual_grade_for_bst_set_definitions [definition, in Sets]
BSTSets.natset [definition, in Sets]
BSTSets.set_insert [definition, in Sets]
BSTSets.union [definition, in Sets]
bst1 [definition, in Trees]
bst2 [definition, in Trees]
bt [inductive, in Trees]
btbase [inductive, in Indprop]
btbase__not_found [lemma, in Indprop]
BTrue [constructor, in Expressions]
btx [inductive, in Indprop]
btx__nat_in_tree [lemma, in Indprop]
bx_right [constructor, in Indprop]
bx_left [constructor, in Indprop]
bx_found [constructor, in Indprop]
BZ [constructor, in Recursion]
b_eleven [definition, in Recursion]
b_nine [definition, in Recursion]
b_three [definition, in Recursion]
b_two [definition, in Recursion]
b_one [definition, in Recursion]
b_zero [definition, in Recursion]
b':108 [binder, in Indprop]
b1:1 [binder, in Lists]
b1:11 [binder, in Lists]
b1:112 [binder, in Cases]
b1:12 [binder, in Intro]
b1:124 [binder, in Cases]
b1:126 [binder, in Cases]
b1:130 [binder, in Cases]
b1:15 [binder, in Intro]
b1:17 [binder, in Expressions]
b1:18 [binder, in Intro]
b1:20 [binder, in Intro]
b1:26 [binder, in Intro]
b1:51 [binder, in Expressions]
b1:60 [binder, in Expressions]
b2:113 [binder, in Cases]
b2:12 [binder, in Lists]
b2:125 [binder, in Cases]
b2:127 [binder, in Cases]
b2:13 [binder, in Intro]
b2:131 [binder, in Cases]
b2:16 [binder, in Intro]
b2:18 [binder, in Expressions]
b2:19 [binder, in Intro]
b2:2 [binder, in Lists]
b2:21 [binder, in Intro]
b2:27 [binder, in Intro]
b2:52 [binder, in Expressions]
b2:61 [binder, in Expressions]
b3:13 [binder, in Lists]
b:10 [binder, in Structures]
b:102 [binder, in Induction]
b:102 [binder, in Cases]
b:106 [binder, in Indprop]
b:11 [binder, in Intro]
b:118 [binder, in Cases]
b:121 [binder, in Cases]
b:122 [binder, in Cases]
b:123 [binder, in Cases]
b:129 [binder, in Cases]
b:13 [binder, in Cases]
b:134 [binder, in Cases]
b:14 [binder, in Cases]
b:15 [binder, in Cases]
b:16 [binder, in Expressions]
b:17 [binder, in Cases]
b:18 [binder, in Indprop2]
b:18 [binder, in Induction]
b:19 [binder, in Cases]
b:22 [binder, in Expressions]
B:23 [binder, in Propositions]
b:24 [binder, in Intro]
b:24 [binder, in Induction]
b:24 [binder, in Cases]
B:25 [binder, in Propositions]
b:26 [binder, in Cases]
B:27 [binder, in Propositions]
b:3 [binder, in Propositions]
b:30 [binder, in Exists]
B:31 [binder, in Propositions]
B:33 [binder, in Propositions]
b:37 [binder, in Recursion]
b:45 [binder, in Induction]
b:46 [binder, in Induction]
b:50 [binder, in Expressions]
b:58 [binder, in Expressions]
B:6 [binder, in Induction2]
B:63 [binder, in Indprop2]
b:64 [binder, in Propositions]
b:67 [binder, in Cases]
B:68 [binder, in Indprop2]
B:68 [binder, in Induction]
b:74 [binder, in Propositions]
B:8 [binder, in Propositions]
b:80 [binder, in Propositions]
B:84 [binder, in Indprop2]
b:9 [binder, in Intro]
b:93 [binder, in Indprop]
b:94 [binder, in Indprop]
b:95 [binder, in Cases]
b:96 [binder, in Induction]
b:96 [binder, in Cases]
b:98 [binder, in Induction]
C
C [constructor, in Intro]Cases [library]
codon [inductive, in Lists]
color [inductive, in Types]
combine [definition, in Lists]
compare [definition, in Trees]
complement [definition, in Intro]
complementary [definition, in Lists]
complementary_complementary' [lemma, in Induction2]
complementary' [definition, in Induction2]
complementary' [definition, in Higherorder]
complement_correct [lemma, in Induction2]
complement_involutive [lemma, in Cases]
cons [constructor, in Structures]
constfun [definition, in Types]
const_empty_list [definition, in Sorting]
contradiction_implies_anything [lemma, in Cases]
contrapositive [lemma, in Cases]
cost:130 [binder, in Structures]
cost:136 [binder, in Structures]
cost:147 [binder, in Cases]
cost:155 [binder, in Cases]
cost:163 [binder, in Cases]
cost:33 [binder, in Higherorder]
cost:41 [binder, in Indprop2]
cost:46 [binder, in Indprop2]
cost:55 [binder, in Types]
cost:62 [binder, in Types]
cost:69 [binder, in Types]
countoddmembers' [definition, in Higherorder]
count:28 [binder, in Structures]
count:33 [binder, in Structures]
count:40 [binder, in Structures]
count:45 [binder, in Structures]
Cys [constructor, in Lists]
c1:133 [binder, in Structures]
c1:140 [binder, in Structures]
c1:151 [binder, in Cases]
c1:58 [binder, in Types]
c1:66 [binder, in Types]
c2:134 [binder, in Structures]
c2:141 [binder, in Structures]
c2:152 [binder, in Cases]
c2:59 [binder, in Types]
c2:67 [binder, in Types]
c3:142 [binder, in Structures]
c3:153 [binder, in Cases]
c3:68 [binder, in Types]
c:10 [binder, in Types]
c:103 [binder, in Cases]
c:119 [binder, in Cases]
c:16 [binder, in Cases]
c:18 [binder, in Cases]
c:20 [binder, in Cases]
c:25 [binder, in Induction]
c:25 [binder, in Cases]
c:27 [binder, in Cases]
c:6 [binder, in Types]
c:65 [binder, in Propositions]
c:75 [binder, in Propositions]
c:8 [binder, in Types]
c:81 [binder, in Propositions]
D
day [inductive, in Intro]default:109 [binder, in Structures]
default:63 [binder, in Sorting2]
DefnFixpoint [module, in Recursion]
DefnFixpoint.double [definition, in Recursion]
DefnFixpoint.pred [definition, in Recursion]
different_all_three [definition, in Trees]
discriminate_ex3 [definition, in Cases]
discriminate_ex2 [lemma, in Cases]
discriminate_ex1 [lemma, in Cases]
dist_exists_or [lemma, in Exists]
dist_not_forall [lemma, in Exists]
dist_not_exists [lemma, in Exists]
dna1:25 [binder, in Higherorder]
dna1:3 [binder, in Lists]
dna1:30 [binder, in Induction2]
dna1:32 [binder, in Induction2]
dna1:35 [binder, in Induction2]
dna1:6 [binder, in Lists]
dna1:75 [binder, in Induction]
dna2:26 [binder, in Higherorder]
dna2:31 [binder, in Induction2]
dna2:33 [binder, in Induction2]
dna2:36 [binder, in Induction2]
dna2:4 [binder, in Lists]
dna2:7 [binder, in Lists]
dna2:76 [binder, in Induction]
dna:27 [binder, in Lists]
dna:34 [binder, in Induction2]
dna:78 [binder, in Induction]
double [definition, in Induction]
double_injective_take2 [lemma, in Induction2]
double_injective_take2_FAILED [lemma, in Induction2]
double_injective [lemma, in Induction2]
double_injective_FAILED [lemma, in Induction2]
double_bin [definition, in Induction]
double_plus [lemma, in Induction]
double_neg [lemma, in Cases]
d:102 [binder, in Sorting2]
d:13 [binder, in Types]
d:21 [binder, in Cases]
d:3 [binder, in Intro]
d:53 [binder, in Types]
d:66 [binder, in Propositions]
d:7 [binder, in Intro]
d:76 [binder, in Propositions]
d:82 [binder, in Propositions]
E
empty [constructor, in Trees]empty_natset [definition, in Sets]
empty_st [definition, in Expressions]
encode [definition, in Lists]
encode_one [definition, in Lists]
enumerate [definition, in Higherorder]
EQ [constructor, in Trees]
eqb [definition, in Types]
eqb_trans [lemma, in Induction2]
eqb_sym [lemma, in Induction2]
eqb_false_iff [lemma, in Induction2]
eqb_true_iff [lemma, in Induction2]
eqb_true [lemma, in Induction2]
eqb_refl [lemma, in Induction]
eqb_0_l [lemma, in Cases]
eq_strand_iff [lemma, in Induction2]
eq_base [definition, in Intro]
eq_strand_refl [lemma, in Induction]
eq_strand [definition, in Induction]
eq_strand [definition, in Lists]
eq_base [definition, in Lists]
eq_base_iff [lemma, in Cases]
eq_base_true [lemma, in Cases]
eq_base_refl [lemma, in Cases]
Errors [module, in Structures]
Errors.BadErrors [module, in Structures]
Errors.BadErrors.FileError_FirstTry [inductive, in Structures]
Errors.BadErrors.file_not_found [constructor, in Structures]
Errors.BadErrors.ok [constructor, in Structures]
Errors.BadErrors.operation_canceled [constructor, in Structures]
Errors.BadErrors.permission_denied [constructor, in Structures]
Errors.BadErrors.temporarily_unavailable [constructor, in Structures]
Errors.Error [constructor, in Structures]
Errors.FileError [inductive, in Structures]
Errors.file_not_found [constructor, in Structures]
Errors.Ok [constructor, in Structures]
Errors.operation_canceled [constructor, in Structures]
Errors.permission_denied [constructor, in Structures]
Errors.read_file [definition, in Structures]
Errors.result [inductive, in Structures]
Errors.result_or_else [definition, in Structures]
Errors.result_transpose [definition, in Structures]
Errors.result_map [definition, in Structures]
Errors.result_to_option [definition, in Structures]
Errors.temporarily_unavailable [constructor, in Structures]
ErrType:154 [binder, in Structures]
Err1:175 [binder, in Structures]
Err2:176 [binder, in Structures]
Err:163 [binder, in Structures]
Err:168 [binder, in Structures]
Err:172 [binder, in Structures]
ev [inductive, in Indprop]
evenb [definition, in Types]
evenb_double_conv [lemma, in Exists]
evenb_double [lemma, in Exists]
evenb_S [lemma, in Exists]
evens_to_ten' [definition, in Sets]
evens_to_ten [definition, in Sets]
even_1000'' [definition, in Exists]
even_1000' [definition, in Exists]
even_1000 [definition, in Exists]
even_bool_prop [lemma, in Exists]
everywhere [definition, in Sorting2]
everywhere_perm [lemma, in Sorting2]
evSS_ev'_subst [lemma, in Indprop]
evSS_ev' [lemma, in Indprop]
evSS_ev [lemma, in Indprop]
evSS_ev [lemma, in Indprop]
ev_plus_plus [lemma, in Indprop]
ev_ev__ev [lemma, in Indprop]
ev_sum [lemma, in Indprop]
ev_even_iff [lemma, in Indprop]
ev_even [lemma, in Indprop]
ev_even_firsttry [lemma, in Indprop]
ev_minus2 [lemma, in Indprop]
ev_inversion [lemma, in Indprop]
ev_double [lemma, in Indprop]
ev_plus4 [lemma, in Indprop]
ev_4' [lemma, in Indprop]
ev_4 [lemma, in Indprop]
ev_SS [constructor, in Indprop]
ev_0 [constructor, in Indprop]
ev5_nonsense [lemma, in Indprop]
excluded_middle [definition, in Exists]
Exists [library]
exists_example_2 [lemma, in Exists]
Expressions [library]
extend_st [definition, in Expressions]
extra_zero [definition, in Sorting]
ex_falso_quodlibet [lemma, in Cases]
e:67 [binder, in Propositions]
e:77 [binder, in Propositions]
e:83 [binder, in Propositions]
e:87 [binder, in Expressions]
F
factorial [definition, in Recursion]false [constructor, in Intro]
favorite_day' [definition, in Structures]
favorite_day [definition, in Types]
fetch_st [definition, in Expressions]
filter [definition, in Higherorder]
filter_even_gt7 [definition, in Higherorder]
filter_preserves_sortedness [lemma, in Sorting2]
filter' [definition, in Higherorder]
first_satisfying [definition, in Higherorder]
flat_map [definition, in Indprop2]
flat_map' [definition, in Higherorder]
flat_map [definition, in Higherorder]
flip [definition, in Types]
fold_left [definition, in Higherorder]
fold_right [definition, in Higherorder]
foo [definition, in Cases]
foo:19 [binder, in Types]
forallb [definition, in Indprop2]
forallb_true_iff [lemma, in Indprop2]
forallb_bt [definition, in Indprop]
four_is_even [lemma, in Exists]
friday [constructor, in Intro]
funny_rec_evenb_0 [lemma, in Cases]
funny_rec [definition, in Cases]
FunSets [module, in Sets]
FunSets.empty_natset [definition, in Sets]
FunSets.intersection [definition, in Sets]
FunSets.manual_grade_for_fun_subset [definition, in Sets]
FunSets.manual_grade_for_fun_remove [definition, in Sets]
FunSets.manual_grade_for_fun_operations [definition, in Sets]
FunSets.member [definition, in Sets]
FunSets.natset [definition, in Sets]
FunSets.set_remove [definition, in Sets]
FunSets.set_insert [definition, in Sets]
FunSets.union [definition, in Sets]
f_equal [lemma, in Induction2]
f7 [definition, in Types]
f:100 [binder, in Higherorder]
f:102 [binder, in Indprop]
f:103 [binder, in Higherorder]
f:112 [binder, in Structures]
f:116 [binder, in Structures]
f:120 [binder, in Structures]
f:145 [binder, in Structures]
f:150 [binder, in Structures]
f:169 [binder, in Structures]
f:177 [binder, in Structures]
f:19 [binder, in Higherorder]
f:25 [binder, in Sorting2]
f:29 [binder, in Higherorder]
f:40 [binder, in Higherorder]
f:46 [binder, in Higherorder]
f:47 [binder, in Types]
f:50 [binder, in Higherorder]
f:52 [binder, in Types]
f:59 [binder, in Higherorder]
f:64 [binder, in Indprop2]
f:66 [binder, in Cases]
f:68 [binder, in Propositions]
f:69 [binder, in Indprop2]
f:69 [binder, in Induction]
f:7 [binder, in Induction2]
f:70 [binder, in Sorting2]
f:73 [binder, in Induction]
f:75 [binder, in Types]
f:76 [binder, in Sorting2]
f:77 [binder, in Higherorder]
f:77 [binder, in Types]
f:78 [binder, in Propositions]
f:78 [binder, in Sorting2]
f:79 [binder, in Indprop2]
f:81 [binder, in Sorting2]
f:82 [binder, in Higherorder]
f:84 [binder, in Propositions]
f:85 [binder, in Indprop2]
f:87 [binder, in Structures]
f:88 [binder, in Higherorder]
f:9 [binder, in Propositions]
f:93 [binder, in Structures]
f:97 [binder, in Higherorder]
G
G [constructor, in Intro]Gln [constructor, in Lists]
Glu [constructor, in Lists]
Gly [constructor, in Lists]
green [constructor, in Types]
GT [constructor, in Trees]
H
half [definition, in Recursion]hd_error [definition, in Structures]
head_only [definition, in Sorting]
Higherorder [library]
Hin:126 [binder, in Indprop2]
His [constructor, in Lists]
Hl:79 [binder, in Indprop]
Hl:99 [binder, in Indprop]
Hne:98 [binder, in Indprop]
Hr:100 [binder, in Indprop]
Hr:84 [binder, in Indprop]
Hxy:58 [binder, in Sorting2]
H12:14 [binder, in Sorting2]
H1:96 [binder, in Indprop2]
H23:15 [binder, in Sorting2]
H2:97 [binder, in Indprop2]
H:117 [binder, in Indprop]
H:121 [binder, in Indprop]
H:127 [binder, in Indprop2]
H:4 [binder, in Indprop]
H:44 [binder, in Indprop]
H:56 [binder, in Indprop]
H:58 [binder, in Indprop]
H:59 [binder, in Indprop2]
H:59 [binder, in Sorting2]
h:62 [binder, in Indprop]
H:65 [binder, in Indprop]
H:7 [binder, in Sorting2]
I
identity_fn_applied_twice [lemma, in Cases]id_list [definition, in Sorting]
iff_trans [lemma, in Cases]
iff_refl [lemma, in Cases]
iff_sym [lemma, in Cases]
Ile [constructor, in Lists]
ill_typed_sort [definition, in Sorting]
impb [definition, in Intro]
implies_PQR [lemma, in Propositions]
In [inductive, in Indprop2]
incr [definition, in Induction]
Indprop [library]
Indprop2 [library]
Induction [library]
Induction2 [library]
injection_discriminate [lemma, in Cases]
injection_ex3 [definition, in Cases]
injection_ex2 [lemma, in Cases]
injection_ex1 [lemma, in Cases]
injective [definition, in Propositions]
inner:33 [binder, in Sets]
inorder [definition, in Trees]
insert [definition, in Trees]
insertion_sort_correct [lemma, in Sorting2]
insert_preserves_setlike [lemma, in Indprop2]
insert_sorted_sorted' [lemma, in Sorting2]
insert_sorted_sorted [lemma, in Sorting2]
insert_sorted_perm [lemma, in Sorting2]
insert_sorted [definition, in Sorting2]
insert_sorted [definition, in Sorting]
insn:76 [binder, in Expressions]
insn:85 [binder, in Expressions]
intersection [definition, in Indprop2]
intersection [definition, in Sets]
Intro [library]
inversion_ex2 [lemma, in Indprop]
inversion_ex1 [lemma, in Indprop]
In_member_iff [lemma, in Indprop2]
In_flat_map [lemma, in Indprop2]
In_app_iff [lemma, in Indprop2]
In_map_iff [lemma, in Indprop2]
In_map [lemma, in Indprop2]
In_example_2 [definition, in Indprop2]
In_example_1 [definition, in Indprop2]
In_cons [constructor, in Indprop2]
In_here [constructor, in Indprop2]
isred [definition, in Types]
isred' [definition, in Types]
is_setlike__setlike [lemma, in Indprop2]
is_setlike [definition, in Indprop2]
is_three [definition, in Propositions]
is_sorted_iff_sorted [lemma, in Sorting2]
is_sorted [definition, in Sorting2]
is_a_sorting_algorithm [definition, in Sorting2]
is_weekday [definition, in Intro]
is_setlike [definition, in Sets]
is_leaf [definition, in Trees]
is_permutation_of [definition, in Sorting]
is_sorted [definition, in Sorting]
is_weekday' [definition, in Types]
is_even_prime [definition, in Exists]
i:1 [binder, in Sorting]
i:104 [binder, in Sorting2]
i:45 [binder, in Sorting2]
i:68 [binder, in Sorting2]
J
j:69 [binder, in Sorting2]j:84 [binder, in Cases]
j:94 [binder, in Cases]
K
k':25 [binder, in Indprop]k':27 [binder, in Indprop]
k:20 [binder, in Exists]
k:22 [binder, in Exists]
k:23 [binder, in Indprop]
k:24 [binder, in Indprop]
k:24 [binder, in Exists]
k:26 [binder, in Indprop]
k:26 [binder, in Exists]
k:27 [binder, in Exists]
k:29 [binder, in Indprop]
k:31 [binder, in Indprop]
k:74 [binder, in Types]
L
leaf [definition, in Trees]leb [definition, in Cases]
leb [definition, in Types]
leb_iff [lemma, in Indprop2]
leb_true_trans [lemma, in Indprop2]
leb_correct [lemma, in Indprop2]
leb_complete [lemma, in Indprop2]
leb_nm__leb_mn' [lemma, in Indprop2]
leb_spec [lemma, in Indprop2]
leb_nm__leb_mn [lemma, in Indprop2]
leb_refl [lemma, in Induction]
lemma_application_ex2 [definition, in Induction]
lemma_application_ex1 [definition, in Induction]
length [definition, in Structures]
length_is_1 [definition, in Higherorder]
length' [definition, in Higherorder]
Leu [constructor, in Lists]
le_plus_l [lemma, in Indprop2]
le_trans [lemma, in Indprop2]
list [inductive, in Structures]
listnum [inductive, in Indprop]
listnum_iff [lemma, in Indprop]
Lists [library]
list123 [definition, in Structures]
list123 [definition, in Lists]
list123' [definition, in Structures]
list123' [definition, in Lists]
list123'' [definition, in Structures]
list123'' [definition, in Lists]
list123''' [definition, in Lists]
ln_cons [constructor, in Indprop]
ln_nil [constructor, in Indprop]
lookup [definition, in Trees]
ls:30 [binder, in Sorting2]
ls:35 [binder, in Sorting2]
lt [definition, in Indprop]
LT [constructor, in Trees]
ltb [definition, in Types]
lt_S [lemma, in Indprop2]
lx:31 [binder, in Lists]
Lys [constructor, in Lists]
ly:32 [binder, in Lists]
l':40 [binder, in Sorting2]
l':44 [binder, in Sorting2]
l':6 [binder, in Sorting2]
l':75 [binder, in Indprop2]
l0 [definition, in Sorting]
l1 [definition, in Sorting]
l1:11 [binder, in Sorting2]
l1:114 [binder, in Indprop2]
l1:118 [binder, in Indprop2]
l1:13 [binder, in Sets]
l1:133 [binder, in Indprop2]
l1:135 [binder, in Indprop2]
l1:16 [binder, in Sets]
l1:19 [binder, in Sorting2]
l1:21 [binder, in Sorting]
l1:22 [binder, in Sorting2]
l1:25 [binder, in Sets]
l1:28 [binder, in Sets]
l1:34 [binder, in Sets]
l1:49 [binder, in Structures]
l1:54 [binder, in Induction]
l1:63 [binder, in Induction]
l1:9 [binder, in Sets]
l2 [definition, in Sorting]
l2:10 [binder, in Sets]
l2:115 [binder, in Indprop2]
l2:119 [binder, in Indprop2]
l2:12 [binder, in Sorting2]
l2:134 [binder, in Indprop2]
l2:136 [binder, in Indprop2]
l2:14 [binder, in Sets]
l2:17 [binder, in Sets]
l2:20 [binder, in Sorting2]
l2:22 [binder, in Sorting]
l2:23 [binder, in Sorting2]
l2:26 [binder, in Sets]
l2:29 [binder, in Sets]
l2:31 [binder, in Sets]
l2:35 [binder, in Sets]
l2:50 [binder, in Structures]
l2:55 [binder, in Induction]
l2:64 [binder, in Induction]
l3 [definition, in Sorting]
l3:13 [binder, in Sorting2]
l3:137 [binder, in Indprop2]
l4 [definition, in Sorting]
l:10 [binder, in Higherorder]
l:10 [binder, in Sorting2]
l:10 [binder, in Sorting]
l:100 [binder, in Indprop2]
l:100 [binder, in Structures]
l:101 [binder, in Higherorder]
l:104 [binder, in Indprop2]
l:104 [binder, in Higherorder]
l:105 [binder, in Structures]
l:106 [binder, in Sorting2]
l:107 [binder, in Sorting2]
l:109 [binder, in Indprop2]
l:109 [binder, in Indprop]
l:11 [binder, in Structures]
l:111 [binder, in Indprop2]
l:12 [binder, in Structures]
l:12 [binder, in Sorting]
l:125 [binder, in Indprop2]
l:129 [binder, in Indprop2]
l:13 [binder, in Higherorder]
l:130 [binder, in Indprop2]
l:132 [binder, in Indprop2]
l:14 [binder, in Sorting]
l:16 [binder, in Higherorder]
l:16 [binder, in Sorting]
l:17 [binder, in Sorting2]
l:18 [binder, in Sorting]
l:19 [binder, in Structures]
l:19 [binder, in Sets]
l:19 [binder, in Sorting]
l:2 [binder, in Sets]
l:2 [binder, in Sorting]
l:20 [binder, in Higherorder]
l:23 [binder, in Structures]
l:23 [binder, in Sets]
l:29 [binder, in Induction2]
l:3 [binder, in Higherorder]
l:30 [binder, in Higherorder]
l:34 [binder, in Higherorder]
l:38 [binder, in Lists]
l:39 [binder, in Sorting2]
l:4 [binder, in Structures]
l:4 [binder, in Trees]
l:4 [binder, in Sorting]
l:41 [binder, in Higherorder]
l:43 [binder, in Sorting2]
l:46 [binder, in Sorting2]
l:47 [binder, in Higherorder]
l:48 [binder, in Induction]
l:49 [binder, in Sorting2]
l:5 [binder, in Sorting2]
l:5 [binder, in Structures]
l:5 [binder, in Sets]
l:52 [binder, in Higherorder]
l:52 [binder, in Induction]
l:54 [binder, in Structures]
l:55 [binder, in Indprop2]
l:57 [binder, in Sorting2]
l:57 [binder, in Structures]
l:58 [binder, in Indprop2]
l:59 [binder, in Structures]
l:6 [binder, in Sorting]
l:61 [binder, in Higherorder]
l:62 [binder, in Sorting2]
l:65 [binder, in Indprop2]
l:66 [binder, in Induction]
l:67 [binder, in Indprop]
l:7 [binder, in Higherorder]
l:70 [binder, in Indprop2]
l:70 [binder, in Induction]
l:72 [binder, in Sorting2]
l:73 [binder, in Indprop]
l:74 [binder, in Indprop2]
l:74 [binder, in Induction]
l:75 [binder, in Sorting2]
l:76 [binder, in Indprop]
l:8 [binder, in Higherorder]
l:8 [binder, in Sets]
l:8 [binder, in Sorting]
l:80 [binder, in Indprop2]
l:81 [binder, in Indprop]
l:83 [binder, in Higherorder]
l:83 [binder, in Sorting2]
l:83 [binder, in Cases]
l:86 [binder, in Indprop2]
l:86 [binder, in Sorting2]
l:89 [binder, in Higherorder]
l:9 [binder, in Higherorder]
l:9 [binder, in Sorting]
l:91 [binder, in Sorting2]
l:92 [binder, in Sorting2]
l:93 [binder, in Higherorder]
l:93 [binder, in Cases]
l:94 [binder, in Sorting2]
l:95 [binder, in Indprop2]
l:95 [binder, in Sorting2]
l:95 [binder, in Indprop]
l:96 [binder, in Sorting2]
l:97 [binder, in Sorting2]
l:98 [binder, in Higherorder]
M
manual_grade_for_mult_S_1_informal [definition, in Propositions]manual_grade_for_or_which_informal [definition, in Propositions]
manual_grade_for_and_PQ_informal [definition, in Propositions]
manual_grade_for_implies_PQR_informal [definition, in Propositions]
manual_grade_for_mult_0_l_informal [definition, in Propositions]
manual_grade_for_nth_error_after_last_informal [definition, in Induction2]
manual_grade_for_fold_practice [definition, in Higherorder]
manual_grade_for_is_classday [definition, in Intro]
manual_grade_for_table [definition, in Intro]
manual_grade_for_xorb [definition, in Intro]
manual_grade_for_impb [definition, in Intro]
manual_grade_for_nandb [definition, in Intro]
manual_grade_for_normalize [definition, in Recursion]
manual_grade_for_nat_to_bin [definition, in Recursion]
manual_grade_for_binary [definition, in Recursion]
manual_grade_for_decreasing [definition, in Recursion]
manual_grade_for_double_plus_informal [definition, in Induction]
manual_grade_for_option_map' [definition, in Structures]
manual_grade_for_list_min [definition, in Structures]
manual_grade_for_currying [definition, in Structures]
manual_grade_for_forall_exists [definition, in Lists]
manual_grade_for_sums_to [definition, in Indprop]
manual_grade_for_ev_sum_informal [definition, in Indprop]
manual_grade_for_set_equal [definition, in Sets]
manual_grade_for_argmin3_min3_eqs_informal [definition, in Cases]
manual_grade_for_injection_discriminate_informal [definition, in Cases]
manual_grade_for_negation_fn_applied_twice [definition, in Cases]
manual_grade_for_contrapositive_informal [definition, in Cases]
manual_grade_for_zero_or_succ_informal [definition, in Cases]
manual_grade_for_and_assoc_informal [definition, in Cases]
manual_grade_for_negb_involutive_informal [definition, in Cases]
manual_grade_for_encodings [definition, in Expressions]
manual_grade_for_is_bst [definition, in Trees]
manual_grade_for_search_property [definition, in Trees]
manual_grade_for_traversals [definition, in Trees]
manual_grade_for_partial_app_minus [definition, in Types]
manual_grade_for_mirror [definition, in Types]
manual_grade_for_ltb [definition, in Types]
manual_grade_for_test_leb [definition, in Types]
map [definition, in Higherorder]
map_option' [definition, in Higherorder]
map_option [definition, in Higherorder]
map_rev [lemma, in Induction]
map_length [lemma, in Induction]
map' [definition, in Higherorder]
member [definition, in Sets]
Met [constructor, in Lists]
min [definition, in Types]
minustwo [definition, in Propositions]
minustwo [definition, in Types]
minus_Sn_m [lemma, in Indprop2]
minus_Sn_n [lemma, in Induction]
minus_diag [lemma, in Induction]
minus_n_O [lemma, in Cases]
min_by' [definition, in Higherorder]
min_by [definition, in Higherorder]
min3 [definition, in Cases]
min3 [definition, in Types]
min3_leb [lemma, in Indprop2]
min3_min [lemma, in Indprop2]
min3' [definition, in Types]
mirror' [definition, in Types]
modus_ponens [lemma, in Propositions]
monday [constructor, in Intro]
monochrome [definition, in Types]
MonoList [module, in Structures]
MonoList.boollist [inductive, in Structures]
MonoList.boollist_length [definition, in Structures]
MonoList.bool_cons [constructor, in Structures]
MonoList.bool_nil [constructor, in Structures]
MonoList.natlist [inductive, in Structures]
MonoList.natlist_length [definition, in Structures]
MonoList.nat_cons [constructor, in Structures]
MonoList.nat_nil [constructor, in Structures]
monotonic [definition, in Sorting2]
monotonic_preserves_sortedness [lemma, in Sorting2]
mult_S_1 [lemma, in Propositions]
mult_0_plus [lemma, in Propositions]
mult_0_l [lemma, in Propositions]
mult_comm [lemma, in Induction]
mult_assoc [lemma, in Induction]
mult_plus_distr_r [lemma, in Induction]
mult_1_l [lemma, in Induction]
mult_0_r [lemma, in Induction]
mult_0_plus' [lemma, in Cases]
MyIff [module, in Cases]
MyIff.iff [definition, in Cases]
_ <-> _ (type_scope) [notation, in Cases]
mynil [definition, in Structures]
mynil [definition, in Structures]
mynil' [definition, in Structures]
MyNot [module, in Cases]
MyNot.not [definition, in Cases]
~ _ (type_scope) [notation, in Cases]
m:1 [binder, in Indprop2]
m:10 [binder, in Indprop2]
m:10 [binder, in Recursion]
m:101 [binder, in Cases]
m:11 [binder, in Induction2]
m:114 [binder, in Indprop]
m:118 [binder, in Indprop]
m:12 [binder, in Indprop2]
m:122 [binder, in Indprop]
m:133 [binder, in Cases]
m:139 [binder, in Cases]
m:14 [binder, in Indprop2]
m:15 [binder, in Recursion]
m:16 [binder, in Indprop2]
m:17 [binder, in Induction2]
m:170 [binder, in Cases]
m:173 [binder, in Cases]
m:19 [binder, in Induction2]
m:19 [binder, in Indprop]
m:2 [binder, in Propositions]
m:2 [binder, in Induction2]
m:2 [binder, in Recursion]
m:2 [binder, in Cases]
m:20 [binder, in Induction]
m:21 [binder, in Indprop2]
m:21 [binder, in Induction2]
m:21 [binder, in Recursion]
m:23 [binder, in Indprop2]
m:24 [binder, in Induction2]
m:25 [binder, in Indprop2]
m:26 [binder, in Induction2]
m:27 [binder, in Indprop2]
m:27 [binder, in Induction]
m:27 [binder, in Trees]
m:29 [binder, in Indprop2]
m:29 [binder, in Cases]
m:29 [binder, in Types]
m:30 [binder, in Induction]
m:32 [binder, in Indprop2]
m:32 [binder, in Cases]
m:32 [binder, in Exists]
m:33 [binder, in Indprop]
m:33 [binder, in Cases]
m:34 [binder, in Cases]
m:34 [binder, in Exists]
m:35 [binder, in Indprop]
m:35 [binder, in Types]
m:37 [binder, in Indprop]
m:38 [binder, in Types]
m:39 [binder, in Indprop2]
m:39 [binder, in Propositions]
m:4 [binder, in Induction2]
m:4 [binder, in Exists]
m:41 [binder, in Propositions]
m:43 [binder, in Induction]
m:43 [binder, in Indprop]
m:44 [binder, in Propositions]
m:45 [binder, in Sets]
m:46 [binder, in Propositions]
m:46 [binder, in Indprop]
m:48 [binder, in Propositions]
m:49 [binder, in Induction]
m:49 [binder, in Cases]
m:5 [binder, in Induction]
m:5 [binder, in Cases]
m:51 [binder, in Cases]
m:52 [binder, in Propositions]
m:53 [binder, in Cases]
m:58 [binder, in Propositions]
m:6 [binder, in Indprop2]
m:6 [binder, in Recursion]
m:7 [binder, in Induction]
m:7 [binder, in Cases]
m:70 [binder, in Cases]
m:71 [binder, in Propositions]
m:72 [binder, in Cases]
m:74 [binder, in Cases]
m:77 [binder, in Cases]
m:8 [binder, in Indprop2]
m:80 [binder, in Induction]
m:82 [binder, in Induction]
m:83 [binder, in Structures]
m:85 [binder, in Induction]
m:87 [binder, in Induction]
m:88 [binder, in Propositions]
m:88 [binder, in Cases]
m:9 [binder, in Induction]
m:9 [binder, in Cases]
m:90 [binder, in Induction]
N
nandb [definition, in Intro]NatPlayground [module, in Types]
NatPlayground.nat [inductive, in Types]
NatPlayground.nat' [inductive, in Types]
NatPlayground.O [constructor, in Types]
NatPlayground.pred [definition, in Types]
NatPlayground.S [constructor, in Types]
NatPlayground.stop [constructor, in Types]
NatPlayground.tick [constructor, in Types]
NatPlayground2 [module, in Recursion]
NatPlayground2.minus [definition, in Recursion]
NatPlayground2.mult [definition, in Recursion]
NatPlayground2.plus [definition, in Recursion]
NatPlayground2.pow [definition, in Recursion]
natset [definition, in Sets]
natset_yikes [definition, in Sets]
nat_bin_nat [lemma, in Induction]
nat_to_bin [definition, in Induction]
nat_in_tree [definition, in Indprop]
negb [definition, in Intro]
negb_involutive [lemma, in Cases]
negb' [definition, in Intro]
next_weekday [definition, in Intro]
next_ev [inductive, in Indprop]
next_nat [inductive, in Indprop]
ne_2 [constructor, in Indprop]
ne_1 [constructor, in Indprop]
nil [constructor, in Structures]
nn [constructor, in Indprop]
node [constructor, in Trees]
non_set_list [definition, in Sets]
non_bst2 [definition, in Trees]
non_bst1 [definition, in Trees]
normalize [definition, in Recursion]
normalize [definition, in Induction]
not_P__P_true [lemma, in Cases]
not_true_iff_false [lemma, in Cases]
not_both_true_and_false [lemma, in Cases]
not_true_is_false' [lemma, in Cases]
not_true_is_false [lemma, in Cases]
not_implies_our_not [lemma, in Cases]
not_False [lemma, in Cases]
not_forall__exists_not [lemma, in Exists]
not_exists__forall_not [lemma, in Exists]
nth [definition, in Sorting2]
nth_error_after_last [lemma, in Induction2]
nth_default [definition, in Sorting2]
nth_in_list [definition, in Sorting2]
nth_error [definition, in Structures]
num_leaves [definition, in Trees]
n_le_m__Sn_le_Sm [lemma, in Indprop2]
n':11 [binder, in Indprop]
n':61 [binder, in Indprop2]
n1:12 [binder, in Induction2]
n1:143 [binder, in Cases]
n1:159 [binder, in Cases]
n1:19 [binder, in Indprop2]
n1:33 [binder, in Indprop2]
n1:36 [binder, in Indprop2]
n1:39 [binder, in Types]
n1:41 [binder, in Types]
n1:44 [binder, in Types]
n2:13 [binder, in Induction2]
n2:144 [binder, in Cases]
n2:160 [binder, in Cases]
n2:20 [binder, in Indprop2]
n2:34 [binder, in Indprop2]
n2:37 [binder, in Indprop2]
n2:40 [binder, in Types]
n2:42 [binder, in Types]
n2:45 [binder, in Types]
n3:145 [binder, in Cases]
n3:161 [binder, in Cases]
n3:35 [binder, in Indprop2]
n3:38 [binder, in Indprop2]
n3:43 [binder, in Types]
n3:46 [binder, in Types]
n:1 [binder, in Propositions]
n:1 [binder, in Induction2]
n:1 [binder, in Recursion]
n:1 [binder, in Induction]
n:1 [binder, in Cases]
n:1 [binder, in Exists]
n:10 [binder, in Induction2]
n:10 [binder, in Indprop]
n:100 [binder, in Cases]
n:101 [binder, in Induction]
n:101 [binder, in Structures]
n:11 [binder, in Indprop2]
n:11 [binder, in Induction]
n:11 [binder, in Cases]
n:115 [binder, in Indprop]
n:119 [binder, in Indprop]
n:12 [binder, in Propositions]
n:12 [binder, in Induction]
n:12 [binder, in Indprop]
n:12 [binder, in Cases]
n:123 [binder, in Indprop]
n:13 [binder, in Indprop2]
n:13 [binder, in Propositions]
n:13 [binder, in Indprop]
n:13 [binder, in Sorting]
n:132 [binder, in Cases]
n:135 [binder, in Cases]
n:136 [binder, in Cases]
n:137 [binder, in Cases]
n:138 [binder, in Cases]
n:14 [binder, in Propositions]
n:14 [binder, in Recursion]
n:14 [binder, in Indprop]
n:15 [binder, in Indprop2]
n:15 [binder, in Propositions]
n:15 [binder, in Induction]
n:15 [binder, in Indprop]
n:16 [binder, in Induction2]
n:16 [binder, in Induction]
n:16 [binder, in Indprop]
n:16 [binder, in Types]
n:167 [binder, in Cases]
n:168 [binder, in Cases]
n:169 [binder, in Cases]
n:17 [binder, in Induction]
n:17 [binder, in Indprop]
n:171 [binder, in Cases]
n:172 [binder, in Cases]
n:18 [binder, in Induction2]
n:18 [binder, in Recursion]
n:18 [binder, in Indprop]
n:19 [binder, in Induction]
n:19 [binder, in Exists]
n:2 [binder, in Indprop2]
n:2 [binder, in Induction]
n:2 [binder, in Exists]
n:20 [binder, in Induction2]
n:20 [binder, in Recursion]
n:20 [binder, in Types]
n:21 [binder, in Indprop]
n:21 [binder, in Exists]
n:22 [binder, in Indprop2]
n:22 [binder, in Induction]
n:22 [binder, in Indprop]
n:22 [binder, in Cases]
n:22 [binder, in Types]
n:23 [binder, in Induction2]
n:23 [binder, in Induction]
n:23 [binder, in Cases]
n:23 [binder, in Exists]
n:24 [binder, in Indprop2]
n:24 [binder, in Higherorder]
n:24 [binder, in Recursion]
n:24 [binder, in Types]
n:25 [binder, in Induction2]
n:25 [binder, in Exists]
n:26 [binder, in Indprop2]
n:26 [binder, in Recursion]
n:26 [binder, in Induction]
n:26 [binder, in Trees]
n:27 [binder, in Induction2]
n:27 [binder, in Types]
n:28 [binder, in Indprop2]
n:28 [binder, in Indprop]
n:28 [binder, in Types]
n:29 [binder, in Recursion]
n:29 [binder, in Induction]
n:29 [binder, in Expressions]
n:3 [binder, in Induction2]
n:3 [binder, in Induction]
n:3 [binder, in Structures]
n:3 [binder, in Indprop]
n:3 [binder, in Cases]
n:3 [binder, in Expressions]
n:30 [binder, in Indprop]
n:31 [binder, in Indprop2]
n:31 [binder, in Recursion]
n:31 [binder, in Trees]
n:31 [binder, in Exists]
n:32 [binder, in Induction]
n:32 [binder, in Indprop]
n:33 [binder, in Exists]
n:34 [binder, in Indprop]
n:34 [binder, in Types]
n:35 [binder, in Recursion]
n:35 [binder, in Cases]
n:35 [binder, in Trees]
n:36 [binder, in Recursion]
n:36 [binder, in Indprop]
n:36 [binder, in Expressions]
n:37 [binder, in Types]
n:38 [binder, in Propositions]
n:38 [binder, in Cases]
n:4 [binder, in Indprop2]
n:4 [binder, in Propositions]
n:4 [binder, in Induction]
n:4 [binder, in Cases]
n:40 [binder, in Propositions]
n:40 [binder, in Trees]
n:41 [binder, in Indprop]
n:41 [binder, in Sets]
n:42 [binder, in Induction]
n:42 [binder, in Indprop]
n:43 [binder, in Propositions]
n:43 [binder, in Higherorder]
n:43 [binder, in Sets]
n:45 [binder, in Propositions]
n:45 [binder, in Indprop]
n:47 [binder, in Propositions]
n:48 [binder, in Cases]
n:48 [binder, in Types]
n:49 [binder, in Indprop]
n:49 [binder, in Types]
n:5 [binder, in Indprop2]
n:5 [binder, in Propositions]
n:5 [binder, in Recursion]
n:5 [binder, in Indprop]
n:50 [binder, in Induction]
n:50 [binder, in Sets]
n:50 [binder, in Cases]
n:50 [binder, in Types]
n:51 [binder, in Propositions]
n:51 [binder, in Types]
n:52 [binder, in Indprop]
n:52 [binder, in Cases]
n:55 [binder, in Indprop]
n:57 [binder, in Propositions]
n:57 [binder, in Indprop]
n:58 [binder, in Cases]
n:6 [binder, in Propositions]
n:6 [binder, in Induction]
n:6 [binder, in Cases]
n:60 [binder, in Indprop2]
n:60 [binder, in Types]
n:61 [binder, in Propositions]
n:61 [binder, in Sorting2]
n:61 [binder, in Structures]
n:61 [binder, in Types]
n:62 [binder, in Propositions]
n:64 [binder, in Indprop]
n:68 [binder, in Indprop]
n:69 [binder, in Cases]
n:7 [binder, in Indprop2]
n:70 [binder, in Propositions]
n:71 [binder, in Cases]
n:72 [binder, in Expressions]
n:73 [binder, in Cases]
n:76 [binder, in Cases]
n:79 [binder, in Induction]
n:8 [binder, in Induction]
n:8 [binder, in Indprop]
n:8 [binder, in Cases]
n:82 [binder, in Sorting2]
n:82 [binder, in Structures]
n:83 [binder, in Induction]
n:84 [binder, in Induction]
n:85 [binder, in Propositions]
n:85 [binder, in Indprop]
n:85 [binder, in Cases]
n:86 [binder, in Cases]
n:87 [binder, in Propositions]
n:87 [binder, in Cases]
n:89 [binder, in Indprop]
n:9 [binder, in Indprop2]
n:9 [binder, in Recursion]
n:9 [binder, in Indprop]
n:93 [binder, in Induction]
O
oddb [definition, in Types]OkType:153 [binder, in Structures]
one_not_even' [lemma, in Indprop]
one_not_even [lemma, in Indprop]
OptionPlayground [module, in Structures]
OptionPlayground.None [constructor, in Structures]
OptionPlayground.option [inductive, in Structures]
OptionPlayground.Some [constructor, in Structures]
option_lift [definition, in Higherorder]
option_or [definition, in Higherorder]
option_map' [definition, in Structures]
option_map [definition, in Structures]
opt:108 [binder, in Structures]
opt:113 [binder, in Structures]
opt:117 [binder, in Structures]
opt:121 [binder, in Structures]
orb [definition, in Intro]
orb_true [lemma, in Induction]
orb_true_3 [lemma, in Cases]
orb_true_iff [lemma, in Cases]
ordering [inductive, in Trees]
or_which [lemma, in Propositions]
or_inclusive2 [lemma, in Propositions]
or_inclusive1 [lemma, in Propositions]
or_intro_r [lemma, in Propositions]
or_intro_l [lemma, in Propositions]
or_assoc [lemma, in Cases]
or_commut' [lemma, in Cases]
or_commut [lemma, in Cases]
or:72 [binder, in Higherorder]
other:50 [binder, in Indprop2]
out:91 [binder, in Higherorder]
out:95 [binder, in Higherorder]
ox:127 [binder, in Structures]
oy:128 [binder, in Structures]
O_le_n [lemma, in Indprop2]
o1:123 [binder, in Structures]
o1:131 [binder, in Structures]
o1:137 [binder, in Structures]
o1:148 [binder, in Cases]
o1:156 [binder, in Cases]
o1:164 [binder, in Cases]
o1:42 [binder, in Indprop2]
o1:47 [binder, in Indprop2]
o1:56 [binder, in Types]
o1:63 [binder, in Types]
o1:70 [binder, in Types]
o2:124 [binder, in Structures]
o2:132 [binder, in Structures]
o2:138 [binder, in Structures]
o2:149 [binder, in Cases]
o2:157 [binder, in Cases]
o2:165 [binder, in Cases]
o2:43 [binder, in Indprop2]
o2:48 [binder, in Indprop2]
o2:57 [binder, in Types]
o2:64 [binder, in Types]
o2:71 [binder, in Types]
o3:139 [binder, in Structures]
o3:150 [binder, in Cases]
o3:158 [binder, in Cases]
o3:166 [binder, in Cases]
o3:44 [binder, in Indprop2]
o3:49 [binder, in Indprop2]
o3:65 [binder, in Types]
o3:72 [binder, in Types]
o:10 [binder, in Cases]
o:116 [binder, in Indprop]
o:120 [binder, in Indprop]
o:124 [binder, in Indprop]
o:20 [binder, in Indprop]
o:3 [binder, in Indprop2]
o:3 [binder, in Exists]
o:30 [binder, in Indprop2]
o:42 [binder, in Propositions]
o:49 [binder, in Propositions]
o:53 [binder, in Propositions]
o:71 [binder, in Higherorder]
o:72 [binder, in Propositions]
o:75 [binder, in Cases]
o:78 [binder, in Cases]
o:89 [binder, in Propositions]
P
pair [constructor, in Structures]PairProjection [module, in Structures]
PairProjection.fst [definition, in Structures]
PairProjection.manual_grade_for_pair_exercises [definition, in Structures]
PairProjection.pair_both [definition, in Structures]
PairProjection.pair_swap [definition, in Structures]
PairProjection.silly_pair [definition, in Structures]
PairProjection.snd [definition, in Structures]
pair:80 [binder, in Structures]
pair:81 [binder, in Structures]
partition [definition, in Higherorder]
path:161 [binder, in Structures]
Permutation [inductive, in Sorting2]
permutations [definition, in Sorting2]
permutations_complete [lemma, in Sorting2]
Permutation_sym [lemma, in Sorting2]
Permutation_length [lemma, in Sorting2]
Permutation_refl [lemma, in Sorting2]
permutation_eg [definition, in Sorting2]
permutation_false_tests [definition, in Sorting]
permutation_true_tests [definition, in Sorting]
perm_trans [constructor, in Sorting2]
perm_swap [constructor, in Sorting2]
perm_skip [constructor, in Sorting2]
perm_nil [constructor, in Sorting2]
Phe [constructor, in Lists]
Playground [module, in Indprop]
Playground.le [inductive, in Indprop]
Playground.le_S [constructor, in Indprop]
Playground.le_n [constructor, in Indprop]
Playground.test_le3 [lemma, in Indprop]
Playground.test_le2 [lemma, in Indprop]
Playground.test_le1 [lemma, in Indprop]
_ <= _ [notation, in Indprop]
plus_lt [lemma, in Indprop2]
plus_id_exercise [lemma, in Propositions]
plus_id_example [lemma, in Propositions]
plus_1_l [lemma, in Propositions]
plus_O_n' [lemma, in Propositions]
plus_O_n [lemma, in Propositions]
plus_fact [definition, in Propositions]
plus_n_Sm [lemma, in Induction2]
plus_swap' [lemma, in Induction]
plus_swap [lemma, in Induction]
plus_comm3_take3 [lemma, in Induction]
plus_comm3_take2 [lemma, in Induction]
plus_comm3 [lemma, in Induction]
plus_ble_compat_l [lemma, in Induction]
plus_assoc [lemma, in Induction]
plus_comm [lemma, in Induction]
plus_n_Sm [lemma, in Induction]
plus_n_O [lemma, in Induction]
plus_1_neq_0' [lemma, in Cases]
plus_1_neq_0 [lemma, in Cases]
plus_1_neq_0_firsttry [lemma, in Cases]
plus' [definition, in Recursion]
plus3 [definition, in Types]
Postscript [library]
Preface [library]
preserves_sortedness [definition, in Sorting2]
primary [constructor, in Types]
Pro [constructor, in Lists]
prod [inductive, in Structures]
prod_uncurry [definition, in Structures]
prod_curry [definition, in Structures]
prog_eg [definition, in Expressions]
prog:79 [binder, in Expressions]
prog:84 [binder, in Expressions]
proj1 [lemma, in Cases]
proj2 [lemma, in Cases]
Propositions [library]
p:10 [binder, in Induction]
P:10 [binder, in Exists]
P:101 [binder, in Sorting2]
P:104 [binder, in Cases]
P:106 [binder, in Cases]
P:108 [binder, in Cases]
P:109 [binder, in Cases]
P:114 [binder, in Cases]
P:128 [binder, in Cases]
P:14 [binder, in Exists]
P:17 [binder, in Propositions]
P:19 [binder, in Propositions]
p:21 [binder, in Induction]
p:22 [binder, in Induction2]
p:24 [binder, in Sorting]
p:27 [binder, in Sorting]
P:28 [binder, in Propositions]
p:28 [binder, in Induction]
P:28 [binder, in Exists]
P:29 [binder, in Exists]
p:31 [binder, in Induction]
P:34 [binder, in Propositions]
P:36 [binder, in Exists]
p:38 [binder, in Indprop]
P:39 [binder, in Cases]
P:40 [binder, in Exists]
P:41 [binder, in Cases]
P:43 [binder, in Cases]
P:45 [binder, in Cases]
p:5 [binder, in Types]
p:50 [binder, in Propositions]
p:54 [binder, in Propositions]
P:54 [binder, in Cases]
P:56 [binder, in Cases]
P:59 [binder, in Cases]
P:6 [binder, in Exists]
P:60 [binder, in Cases]
P:61 [binder, in Cases]
P:63 [binder, in Cases]
P:64 [binder, in Cases]
p:71 [binder, in Structures]
p:75 [binder, in Structures]
p:81 [binder, in Induction]
p:86 [binder, in Induction]
p:87 [binder, in Sorting2]
p:89 [binder, in Sorting2]
p:90 [binder, in Propositions]
P:92 [binder, in Indprop2]
P:93 [binder, in Indprop2]
p:94 [binder, in Structures]
P:97 [binder, in Cases]
P:99 [binder, in Indprop2]
P:99 [binder, in Cases]
Q
Q:105 [binder, in Cases]Q:107 [binder, in Cases]
Q:110 [binder, in Cases]
Q:115 [binder, in Cases]
Q:15 [binder, in Exists]
Q:18 [binder, in Propositions]
Q:20 [binder, in Propositions]
Q:29 [binder, in Propositions]
Q:35 [binder, in Propositions]
Q:40 [binder, in Cases]
Q:42 [binder, in Cases]
Q:44 [binder, in Cases]
Q:46 [binder, in Cases]
q:55 [binder, in Propositions]
Q:55 [binder, in Cases]
Q:57 [binder, in Cases]
q:59 [binder, in Propositions]
Q:62 [binder, in Cases]
Q:65 [binder, in Cases]
Q:98 [binder, in Cases]
R
R [module, in Indprop]Recursion [library]
red [constructor, in Types]
remove [definition, in Trees]
remove_min [definition, in Trees]
remove_all [definition, in Sorting]
repeat [definition, in Structures]
repeat' [definition, in Structures]
repeat'' [definition, in Structures]
repeat''' [definition, in Structures]
restricted_excluded_middle_eq [lemma, in Exists]
restricted_excluded_middle [lemma, in Exists]
rev [definition, in Structures]
rev_involutive [lemma, in Induction]
rev_app_distr [lemma, in Induction]
rgb [inductive, in Types]
root [definition, in Trees]
R.c1 [constructor, in Indprop]
R.c2 [constructor, in Indprop]
R.c3 [constructor, in Indprop]
R.fR [definition, in Indprop]
R.manual_grade_for_R_fact [definition, in Indprop]
R.R [inductive, in Indprop]
R.R_equiv_fR [lemma, in Indprop]
R:111 [binder, in Cases]
R:116 [binder, in Cases]
r:164 [binder, in Structures]
r:170 [binder, in Structures]
r:173 [binder, in Structures]
r:178 [binder, in Structures]
R:21 [binder, in Propositions]
R:47 [binder, in Cases]
r:56 [binder, in Propositions]
r:6 [binder, in Trees]
r:60 [binder, in Propositions]
r:74 [binder, in Indprop]
r:77 [binder, in Indprop]
r:82 [binder, in Indprop]
r:97 [binder, in Indprop]
S
same_post_in [definition, in Trees]same_pre_in [definition, in Trees]
saturday [constructor, in Intro]
seed:51 [binder, in Higherorder]
seed:60 [binder, in Higherorder]
select [definition, in Structures]
Ser [constructor, in Lists]
setlike [inductive, in Indprop2]
setlike_eg2 [definition, in Indprop2]
setlike_eg1 [definition, in Indprop2]
setlike_cons [constructor, in Indprop2]
setlike_nil [constructor, in Indprop2]
Sets [library]
set_insert [definition, in Sets]
sillyfun [definition, in Cases]
sillyfun_false [lemma, in Cases]
sillyfun1 [definition, in Cases]
sillyfun1_odd [lemma, in Cases]
sillyfun1_odd_FAILED [lemma, in Cases]
silly_ex [lemma, in Propositions]
silly_fact_2' [lemma, in Cases]
silly_fact_2 [lemma, in Cases]
silly_fact_2_FAILED [lemma, in Cases]
silly_fact_1 [lemma, in Cases]
silly1 [lemma, in Propositions]
silly2 [lemma, in Propositions]
silly2a [lemma, in Propositions]
silly3_firsttry [lemma, in Propositions]
silly3' [lemma, in Cases]
sinstr [inductive, in Expressions]
size [definition, in Induction]
size [definition, in Trees]
size_length_inorder [lemma, in Induction]
SLoad [constructor, in Expressions]
SMinus [constructor, in Expressions]
SMult [constructor, in Expressions]
Sn_le_Sm__n_le_m [lemma, in Indprop2]
sort [definition, in Sorting2]
sort [definition, in Sorting]
sorted [inductive, in Sorting2]
SortedSets [module, in Sets]
SortedSets.empty_natset [definition, in Sets]
SortedSets.is_setlike [definition, in Sets]
SortedSets.member [definition, in Sets]
SortedSets.subset [definition, in Sets]
SortedSets.union [definition, in Sets]
SortedSets.union [definition, in Sets]
sorted_sorted' [lemma, in Sorting2]
sorted_filter_cons [lemma, in Sorting2]
sorted_smaller [lemma, in Sorting2]
sorted_one_through_four [definition, in Sorting2]
sorted_cons [constructor, in Sorting2]
sorted_1 [constructor, in Sorting2]
sorted_nil [constructor, in Sorting2]
sorted' [definition, in Sorting2]
sorted'_sorted [lemma, in Sorting2]
Sorting [library]
Sorting2 [library]
sort_sorted' [lemma, in Sorting2]
sort_idempotent [lemma, in Sorting2]
sort_already_sorted [lemma, in Sorting2]
sort_sorted [lemma, in Sorting2]
sort_perm [lemma, in Sorting2]
split [definition, in Lists]
SPlus [constructor, in Expressions]
SPush [constructor, in Expressions]
sq [constructor, in Indprop]
square [definition, in Cases]
square_of [inductive, in Indprop]
square_mult [lemma, in Cases]
SSSSev__even [lemma, in Indprop]
stack:75 [binder, in Expressions]
stack:78 [binder, in Expressions]
stack:83 [binder, in Expressions]
stack:86 [binder, in Expressions]
state [definition, in Expressions]
STOP [constructor, in Lists]
strand [definition, in Lists]
Structures [library]
st:27 [binder, in Expressions]
st:30 [binder, in Expressions]
st:53 [binder, in Expressions]
st:57 [binder, in Expressions]
st:74 [binder, in Expressions]
st:77 [binder, in Expressions]
st:82 [binder, in Expressions]
subset [definition, in Indprop2]
subset [definition, in Sets]
sum [definition, in Structures]
sum [definition, in Indprop]
sunday [constructor, in Intro]
S_nbeq_0 [lemma, in Induction]
S_inj [lemma, in Cases]
S_injective' [lemma, in Cases]
S_injective [lemma, in Cases]
s_compile [definition, in Expressions]
s_execute' [definition, in Expressions]
s_execute [definition, in Expressions]
s_insn [definition, in Expressions]
s:42 [binder, in Sets]
s:44 [binder, in Sets]
s:51 [binder, in Sets]
T
T [constructor, in Intro]test:103 [binder, in Indprop2]
test:108 [binder, in Indprop2]
test:12 [binder, in Higherorder]
test:2 [binder, in Higherorder]
third [definition, in Recursion]
Thr [constructor, in Lists]
thursday [constructor, in Intro]
trans_eq_exercise [definition, in Propositions]
trans_eq_example'' [definition, in Propositions]
trans_eq_example' [definition, in Propositions]
trans_eq [lemma, in Propositions]
trans_eq_example [definition, in Propositions]
Trees [library]
Trp [constructor, in Lists]
true [constructor, in Intro]
True_or_r [lemma, in Propositions]
True_or_l [lemma, in Propositions]
True_and_id [lemma, in Propositions]
True_is_true' [lemma, in Propositions]
True_is_true [lemma, in Propositions]
tuesday [constructor, in Intro]
twice [definition, in Types]
Types [library]
Tyr [constructor, in Lists]
t':33 [binder, in Sorting2]
t1:37 [binder, in Sets]
t1:46 [binder, in Sets]
t1:48 [binder, in Sets]
T2 [constructor, in Recursion]
T2P1 [constructor, in Recursion]
t2:38 [binder, in Sets]
t2:47 [binder, in Sets]
t2:49 [binder, in Sets]
t:103 [binder, in Indprop]
t:107 [binder, in Indprop]
t:11 [binder, in Trees]
t:13 [binder, in Trees]
t:16 [binder, in Trees]
t:21 [binder, in Trees]
t:32 [binder, in Trees]
t:36 [binder, in Trees]
t:38 [binder, in Trees]
t:41 [binder, in Trees]
t:57 [binder, in Induction]
t:61 [binder, in Induction]
t:63 [binder, in Indprop]
t:8 [binder, in Trees]
t:86 [binder, in Indprop]
T:89 [binder, in Indprop2]
t:90 [binder, in Indprop]
t:94 [binder, in Indprop2]
T:98 [binder, in Indprop2]
U
union [definition, in Sets]union_intersection_dist [lemma, in Indprop2]
union_preserves_setlike [lemma, in Indprop2]
unique [definition, in Sorting]
unique_sort [definition, in Sorting]
unwrap_or [definition, in Structures]
u_eleven [definition, in Recursion]
u_nine [definition, in Recursion]
u_three [definition, in Recursion]
u_two [definition, in Recursion]
u_one [definition, in Recursion]
u_zero [definition, in Recursion]
V
Val [constructor, in Lists]v:19 [binder, in Trees]
v:5 [binder, in Trees]
v:78 [binder, in Indprop]
v:83 [binder, in Indprop]
v:96 [binder, in Indprop]
W
W [definition, in Expressions]wednesday [constructor, in Intro]
white [constructor, in Types]
wrong_ev_SS [constructor, in Indprop]
wrong_ev_0 [constructor, in Indprop]
wrong_ev [inductive, in Indprop]
X
X [definition, in Expressions]xor_option [definition, in Structures]
X:1 [binder, in Higherorder]
x:1 [binder, in Sets]
X:1 [binder, in Trees]
x:10 [binder, in Propositions]
X:10 [binder, in Trees]
x:101 [binder, in Indprop2]
X:101 [binder, in Indprop]
X:102 [binder, in Indprop2]
X:102 [binder, in Higherorder]
X:104 [binder, in Structures]
x:105 [binder, in Higherorder]
x:106 [binder, in Higherorder]
X:106 [binder, in Structures]
X:107 [binder, in Indprop2]
X:107 [binder, in Structures]
X:11 [binder, in Higherorder]
x:11 [binder, in Exists]
x:110 [binder, in Indprop2]
X:110 [binder, in Structures]
X:114 [binder, in Structures]
X:118 [binder, in Structures]
X:12 [binder, in Trees]
x:12 [binder, in Exists]
X:122 [binder, in Structures]
x:124 [binder, in Indprop2]
X:125 [binder, in Structures]
x:128 [binder, in Indprop2]
X:13 [binder, in Exists]
x:131 [binder, in Indprop2]
x:14 [binder, in Induction2]
x:14 [binder, in Higherorder]
X:143 [binder, in Structures]
x:146 [binder, in Structures]
x:149 [binder, in Structures]
X:15 [binder, in Higherorder]
X:15 [binder, in Structures]
X:15 [binder, in Trees]
x:157 [binder, in Structures]
x:158 [binder, in Structures]
x:16 [binder, in Exists]
X:162 [binder, in Structures]
X:166 [binder, in Structures]
X:17 [binder, in Higherorder]
x:17 [binder, in Exists]
X:171 [binder, in Structures]
X:174 [binder, in Structures]
x:18 [binder, in Structures]
X:18 [binder, in Trees]
x:18 [binder, in Exists]
X:20 [binder, in Structures]
X:20 [binder, in Trees]
X:21 [binder, in Structures]
X:22 [binder, in Structures]
x:22 [binder, in Sets]
x:23 [binder, in Higherorder]
x:25 [binder, in Sorting]
X:26 [binder, in Structures]
X:27 [binder, in Higherorder]
x:27 [binder, in Structures]
X:28 [binder, in Induction2]
x:28 [binder, in Cases]
x:28 [binder, in Expressions]
x:28 [binder, in Sorting]
X:29 [binder, in Lists]
x:30 [binder, in Cases]
X:31 [binder, in Structures]
x:31 [binder, in Expressions]
X:32 [binder, in Higherorder]
x:32 [binder, in Structures]
x:33 [binder, in Induction]
X:35 [binder, in Exists]
x:36 [binder, in Higherorder]
x:36 [binder, in Induction]
X:36 [binder, in Structures]
X:36 [binder, in Lists]
x:37 [binder, in Higherorder]
X:37 [binder, in Structures]
x:37 [binder, in Expressions]
x:37 [binder, in Exists]
X:38 [binder, in Higherorder]
X:38 [binder, in Structures]
x:38 [binder, in Exists]
x:39 [binder, in Induction]
x:39 [binder, in Structures]
X:39 [binder, in Exists]
x:4 [binder, in Sorting2]
x:41 [binder, in Sorting2]
x:41 [binder, in Exists]
x:42 [binder, in Exists]
X:43 [binder, in Structures]
X:44 [binder, in Higherorder]
x:44 [binder, in Structures]
X:48 [binder, in Higherorder]
X:48 [binder, in Structures]
X:5 [binder, in Exists]
X:51 [binder, in Induction]
X:53 [binder, in Induction]
X:53 [binder, in Structures]
x:54 [binder, in Indprop2]
x:54 [binder, in Sorting2]
x:55 [binder, in Higherorder]
x:55 [binder, in Sorting2]
x:56 [binder, in Indprop2]
X:56 [binder, in Induction]
X:57 [binder, in Higherorder]
X:59 [binder, in Indprop]
X:6 [binder, in Higherorder]
X:60 [binder, in Sorting2]
X:60 [binder, in Induction]
X:62 [binder, in Induction]
X:62 [binder, in Structures]
X:63 [binder, in Structures]
x:64 [binder, in Higherorder]
X:65 [binder, in Induction]
x:66 [binder, in Indprop2]
X:66 [binder, in Indprop]
x:67 [binder, in Higherorder]
x:67 [binder, in Structures]
x:68 [binder, in Cases]
X:69 [binder, in Propositions]
X:69 [binder, in Structures]
X:69 [binder, in Indprop]
x:7 [binder, in Sets]
X:7 [binder, in Trees]
x:7 [binder, in Exists]
X:70 [binder, in Higherorder]
X:71 [binder, in Induction]
x:72 [binder, in Indprop2]
x:72 [binder, in Indprop]
X:73 [binder, in Structures]
x:73 [binder, in Expressions]
x:73 [binder, in Types]
x:74 [binder, in Higherorder]
x:75 [binder, in Indprop]
X:76 [binder, in Higherorder]
x:76 [binder, in Structures]
x:76 [binder, in Types]
X:77 [binder, in Indprop2]
x:78 [binder, in Higherorder]
X:78 [binder, in Structures]
x:78 [binder, in Types]
x:79 [binder, in Higherorder]
x:79 [binder, in Sorting2]
X:79 [binder, in Cases]
x:8 [binder, in Induction2]
x:8 [binder, in Sorting2]
x:8 [binder, in Exists]
x:80 [binder, in Indprop]
x:80 [binder, in Cases]
X:81 [binder, in Higherorder]
x:84 [binder, in Higherorder]
x:84 [binder, in Sorting2]
X:84 [binder, in Structures]
X:86 [binder, in Higherorder]
x:88 [binder, in Indprop2]
x:88 [binder, in Sorting2]
x:88 [binder, in Structures]
X:89 [binder, in Cases]
X:9 [binder, in Exists]
x:90 [binder, in Higherorder]
x:90 [binder, in Sorting2]
X:90 [binder, in Structures]
x:90 [binder, in Cases]
X:92 [binder, in Higherorder]
x:94 [binder, in Higherorder]
X:95 [binder, in Structures]
X:96 [binder, in Higherorder]
x:98 [binder, in Structures]
X:99 [binder, in Higherorder]
X:99 [binder, in Structures]
Y
Y [definition, in Expressions]y1:147 [binder, in Structures]
y2:148 [binder, in Structures]
y:11 [binder, in Propositions]
Y:111 [binder, in Structures]
Y:115 [binder, in Structures]
Y:119 [binder, in Structures]
Y:126 [binder, in Structures]
Y:144 [binder, in Structures]
y:15 [binder, in Induction2]
Y:167 [binder, in Structures]
Y:18 [binder, in Higherorder]
y:26 [binder, in Sorting]
Y:28 [binder, in Higherorder]
y:29 [binder, in Sorting]
Y:30 [binder, in Lists]
y:34 [binder, in Induction]
y:37 [binder, in Induction]
Y:37 [binder, in Lists]
Y:39 [binder, in Higherorder]
y:40 [binder, in Induction]
Y:45 [binder, in Higherorder]
Y:49 [binder, in Higherorder]
y:56 [binder, in Higherorder]
y:56 [binder, in Sorting2]
y:57 [binder, in Indprop2]
Y:58 [binder, in Higherorder]
Y:64 [binder, in Structures]
y:68 [binder, in Structures]
Y:70 [binder, in Structures]
y:71 [binder, in Indprop2]
Y:72 [binder, in Induction]
Y:74 [binder, in Structures]
y:77 [binder, in Structures]
Y:78 [binder, in Indprop2]
Y:79 [binder, in Structures]
y:80 [binder, in Sorting2]
y:81 [binder, in Cases]
y:85 [binder, in Sorting2]
Y:85 [binder, in Structures]
y:87 [binder, in Indprop2]
Y:87 [binder, in Higherorder]
y:89 [binder, in Structures]
y:9 [binder, in Induction2]
y:9 [binder, in Sorting2]
Y:91 [binder, in Structures]
y:91 [binder, in Cases]
Z
Z [definition, in Expressions]zero_nbeq_S [lemma, in Induction]
zero_to_n [definition, in Structures]
zero_not_one' [lemma, in Cases]
zero_not_one [lemma, in Cases]
zero_or_succ [lemma, in Cases]
z:35 [binder, in Induction]
z:38 [binder, in Induction]
z:41 [binder, in Induction]
z:82 [binder, in Cases]
Z:86 [binder, in Structures]
Z:92 [binder, in Structures]
z:92 [binder, in Cases]
_
_n:40 [binder, in Sets]other
_ * _ (nat_scope) [notation, in Recursion]_ - _ (nat_scope) [notation, in Recursion]
_ + _ (nat_scope) [notation, in Recursion]
_ * _ (type_scope) [notation, in Structures]
_ || _ [notation, in Intro]
_ && _ [notation, in Intro]
_ ++ _ [notation, in Lists]
_ :: _ [notation, in Lists]
_ < _ [notation, in Indprop]
( _ , _ ) [notation, in Structures]
[ _ ; .. ; _ ] [notation, in Lists]
[ ] [notation, in Lists]
Notation Index
M
_ <-> _ (type_scope) [in Cases]~ _ (type_scope) [in Cases]
P
_ <= _ [in Indprop]other
_ * _ (nat_scope) [in Recursion]_ - _ (nat_scope) [in Recursion]
_ + _ (nat_scope) [in Recursion]
_ * _ (type_scope) [in Structures]
_ || _ [in Intro]
_ && _ [in Intro]
_ ++ _ [in Lists]
_ :: _ [in Lists]
_ < _ [in Indprop]
( _ , _ ) [in Structures]
[ _ ; .. ; _ ] [in Lists]
[ ] [in Lists]
Binder Index
A
al:103 [in Sorting2]al:26 [in Sorting2]
al:67 [in Sorting2]
al:71 [in Sorting2]
al:77 [in Sorting2]
al:98 [in Sorting2]
al:99 [in Sorting2]
a1:12 [in Expressions]
a1:14 [in Expressions]
a1:38 [in Expressions]
a1:4 [in Expressions]
a1:40 [in Expressions]
a1:42 [in Expressions]
a1:46 [in Expressions]
a1:48 [in Expressions]
a1:6 [in Expressions]
a1:62 [in Expressions]
a1:64 [in Expressions]
a1:66 [in Expressions]
a1:68 [in Expressions]
a1:8 [in Expressions]
a2:13 [in Expressions]
a2:15 [in Expressions]
a2:39 [in Expressions]
a2:41 [in Expressions]
a2:43 [in Expressions]
a2:47 [in Expressions]
a2:49 [in Expressions]
a2:5 [in Expressions]
a2:63 [in Expressions]
a2:65 [in Expressions]
a2:67 [in Expressions]
a2:69 [in Expressions]
a2:7 [in Expressions]
a2:9 [in Expressions]
A:1 [in Sorting2]
A:100 [in Sorting2]
a:105 [in Sorting2]
a:117 [in Cases]
a:120 [in Cases]
A:129 [in Structures]
A:135 [in Structures]
A:146 [in Cases]
A:154 [in Cases]
A:16 [in Propositions]
A:16 [in Sorting2]
A:162 [in Cases]
a:17 [in Indprop2]
A:18 [in Sorting2]
a:19 [in Expressions]
A:21 [in Sorting2]
A:22 [in Propositions]
A:24 [in Propositions]
A:24 [in Sorting2]
a:24 [in Expressions]
A:26 [in Propositions]
A:28 [in Sorting2]
a:29 [in Sorting2]
A:30 [in Propositions]
A:32 [in Propositions]
A:34 [in Sorting2]
A:36 [in Propositions]
A:37 [in Propositions]
A:38 [in Sorting2]
A:40 [in Indprop2]
A:42 [in Sorting2]
a:44 [in Induction]
A:45 [in Indprop2]
A:47 [in Induction]
A:5 [in Induction2]
A:51 [in Indprop2]
a:54 [in Expressions]
A:62 [in Indprop2]
a:63 [in Propositions]
A:67 [in Indprop2]
A:67 [in Induction]
A:7 [in Propositions]
A:73 [in Indprop2]
a:73 [in Propositions]
a:76 [in Indprop2]
a:79 [in Propositions]
A:83 [in Indprop2]
a:93 [in Sorting2]
B
best:65 [in Higherorder]best:68 [in Higherorder]
best:75 [in Higherorder]
best:80 [in Higherorder]
best:85 [in Higherorder]
bl:27 [in Sorting2]
b':108 [in Indprop]
b1:1 [in Lists]
b1:11 [in Lists]
b1:112 [in Cases]
b1:12 [in Intro]
b1:124 [in Cases]
b1:126 [in Cases]
b1:130 [in Cases]
b1:15 [in Intro]
b1:17 [in Expressions]
b1:18 [in Intro]
b1:20 [in Intro]
b1:26 [in Intro]
b1:51 [in Expressions]
b1:60 [in Expressions]
b2:113 [in Cases]
b2:12 [in Lists]
b2:125 [in Cases]
b2:127 [in Cases]
b2:13 [in Intro]
b2:131 [in Cases]
b2:16 [in Intro]
b2:18 [in Expressions]
b2:19 [in Intro]
b2:2 [in Lists]
b2:21 [in Intro]
b2:27 [in Intro]
b2:52 [in Expressions]
b2:61 [in Expressions]
b3:13 [in Lists]
b:10 [in Structures]
b:102 [in Induction]
b:102 [in Cases]
b:106 [in Indprop]
b:11 [in Intro]
b:118 [in Cases]
b:121 [in Cases]
b:122 [in Cases]
b:123 [in Cases]
b:129 [in Cases]
b:13 [in Cases]
b:134 [in Cases]
b:14 [in Cases]
b:15 [in Cases]
b:16 [in Expressions]
b:17 [in Cases]
b:18 [in Indprop2]
b:18 [in Induction]
b:19 [in Cases]
b:22 [in Expressions]
B:23 [in Propositions]
b:24 [in Intro]
b:24 [in Induction]
b:24 [in Cases]
B:25 [in Propositions]
b:26 [in Cases]
B:27 [in Propositions]
b:3 [in Propositions]
b:30 [in Exists]
B:31 [in Propositions]
B:33 [in Propositions]
b:37 [in Recursion]
b:45 [in Induction]
b:46 [in Induction]
b:50 [in Expressions]
b:58 [in Expressions]
B:6 [in Induction2]
B:63 [in Indprop2]
b:64 [in Propositions]
b:67 [in Cases]
B:68 [in Indprop2]
B:68 [in Induction]
b:74 [in Propositions]
B:8 [in Propositions]
b:80 [in Propositions]
B:84 [in Indprop2]
b:9 [in Intro]
b:93 [in Indprop]
b:94 [in Indprop]
b:95 [in Cases]
b:96 [in Induction]
b:96 [in Cases]
b:98 [in Induction]
C
cost:130 [in Structures]cost:136 [in Structures]
cost:147 [in Cases]
cost:155 [in Cases]
cost:163 [in Cases]
cost:33 [in Higherorder]
cost:41 [in Indprop2]
cost:46 [in Indprop2]
cost:55 [in Types]
cost:62 [in Types]
cost:69 [in Types]
count:28 [in Structures]
count:33 [in Structures]
count:40 [in Structures]
count:45 [in Structures]
c1:133 [in Structures]
c1:140 [in Structures]
c1:151 [in Cases]
c1:58 [in Types]
c1:66 [in Types]
c2:134 [in Structures]
c2:141 [in Structures]
c2:152 [in Cases]
c2:59 [in Types]
c2:67 [in Types]
c3:142 [in Structures]
c3:153 [in Cases]
c3:68 [in Types]
c:10 [in Types]
c:103 [in Cases]
c:119 [in Cases]
c:16 [in Cases]
c:18 [in Cases]
c:20 [in Cases]
c:25 [in Induction]
c:25 [in Cases]
c:27 [in Cases]
c:6 [in Types]
c:65 [in Propositions]
c:75 [in Propositions]
c:8 [in Types]
c:81 [in Propositions]
D
default:109 [in Structures]default:63 [in Sorting2]
dna1:25 [in Higherorder]
dna1:3 [in Lists]
dna1:30 [in Induction2]
dna1:32 [in Induction2]
dna1:35 [in Induction2]
dna1:6 [in Lists]
dna1:75 [in Induction]
dna2:26 [in Higherorder]
dna2:31 [in Induction2]
dna2:33 [in Induction2]
dna2:36 [in Induction2]
dna2:4 [in Lists]
dna2:7 [in Lists]
dna2:76 [in Induction]
dna:27 [in Lists]
dna:34 [in Induction2]
dna:78 [in Induction]
d:102 [in Sorting2]
d:13 [in Types]
d:21 [in Cases]
d:3 [in Intro]
d:53 [in Types]
d:66 [in Propositions]
d:7 [in Intro]
d:76 [in Propositions]
d:82 [in Propositions]
E
ErrType:154 [in Structures]Err1:175 [in Structures]
Err2:176 [in Structures]
Err:163 [in Structures]
Err:168 [in Structures]
Err:172 [in Structures]
e:67 [in Propositions]
e:77 [in Propositions]
e:83 [in Propositions]
e:87 [in Expressions]
F
foo:19 [in Types]f:100 [in Higherorder]
f:102 [in Indprop]
f:103 [in Higherorder]
f:112 [in Structures]
f:116 [in Structures]
f:120 [in Structures]
f:145 [in Structures]
f:150 [in Structures]
f:169 [in Structures]
f:177 [in Structures]
f:19 [in Higherorder]
f:25 [in Sorting2]
f:29 [in Higherorder]
f:40 [in Higherorder]
f:46 [in Higherorder]
f:47 [in Types]
f:50 [in Higherorder]
f:52 [in Types]
f:59 [in Higherorder]
f:64 [in Indprop2]
f:66 [in Cases]
f:68 [in Propositions]
f:69 [in Indprop2]
f:69 [in Induction]
f:7 [in Induction2]
f:70 [in Sorting2]
f:73 [in Induction]
f:75 [in Types]
f:76 [in Sorting2]
f:77 [in Higherorder]
f:77 [in Types]
f:78 [in Propositions]
f:78 [in Sorting2]
f:79 [in Indprop2]
f:81 [in Sorting2]
f:82 [in Higherorder]
f:84 [in Propositions]
f:85 [in Indprop2]
f:87 [in Structures]
f:88 [in Higherorder]
f:9 [in Propositions]
f:93 [in Structures]
f:97 [in Higherorder]
H
Hin:126 [in Indprop2]Hl:79 [in Indprop]
Hl:99 [in Indprop]
Hne:98 [in Indprop]
Hr:100 [in Indprop]
Hr:84 [in Indprop]
Hxy:58 [in Sorting2]
H12:14 [in Sorting2]
H1:96 [in Indprop2]
H23:15 [in Sorting2]
H2:97 [in Indprop2]
H:117 [in Indprop]
H:121 [in Indprop]
H:127 [in Indprop2]
H:4 [in Indprop]
H:44 [in Indprop]
H:56 [in Indprop]
H:58 [in Indprop]
H:59 [in Indprop2]
H:59 [in Sorting2]
h:62 [in Indprop]
H:65 [in Indprop]
H:7 [in Sorting2]
I
inner:33 [in Sets]insn:76 [in Expressions]
insn:85 [in Expressions]
i:1 [in Sorting]
i:104 [in Sorting2]
i:45 [in Sorting2]
i:68 [in Sorting2]
J
j:69 [in Sorting2]j:84 [in Cases]
j:94 [in Cases]
K
k':25 [in Indprop]k':27 [in Indprop]
k:20 [in Exists]
k:22 [in Exists]
k:23 [in Indprop]
k:24 [in Indprop]
k:24 [in Exists]
k:26 [in Indprop]
k:26 [in Exists]
k:27 [in Exists]
k:29 [in Indprop]
k:31 [in Indprop]
k:74 [in Types]
L
ls:30 [in Sorting2]ls:35 [in Sorting2]
lx:31 [in Lists]
ly:32 [in Lists]
l':40 [in Sorting2]
l':44 [in Sorting2]
l':6 [in Sorting2]
l':75 [in Indprop2]
l1:11 [in Sorting2]
l1:114 [in Indprop2]
l1:118 [in Indprop2]
l1:13 [in Sets]
l1:133 [in Indprop2]
l1:135 [in Indprop2]
l1:16 [in Sets]
l1:19 [in Sorting2]
l1:21 [in Sorting]
l1:22 [in Sorting2]
l1:25 [in Sets]
l1:28 [in Sets]
l1:34 [in Sets]
l1:49 [in Structures]
l1:54 [in Induction]
l1:63 [in Induction]
l1:9 [in Sets]
l2:10 [in Sets]
l2:115 [in Indprop2]
l2:119 [in Indprop2]
l2:12 [in Sorting2]
l2:134 [in Indprop2]
l2:136 [in Indprop2]
l2:14 [in Sets]
l2:17 [in Sets]
l2:20 [in Sorting2]
l2:22 [in Sorting]
l2:23 [in Sorting2]
l2:26 [in Sets]
l2:29 [in Sets]
l2:31 [in Sets]
l2:35 [in Sets]
l2:50 [in Structures]
l2:55 [in Induction]
l2:64 [in Induction]
l3:13 [in Sorting2]
l3:137 [in Indprop2]
l:10 [in Higherorder]
l:10 [in Sorting2]
l:10 [in Sorting]
l:100 [in Indprop2]
l:100 [in Structures]
l:101 [in Higherorder]
l:104 [in Indprop2]
l:104 [in Higherorder]
l:105 [in Structures]
l:106 [in Sorting2]
l:107 [in Sorting2]
l:109 [in Indprop2]
l:109 [in Indprop]
l:11 [in Structures]
l:111 [in Indprop2]
l:12 [in Structures]
l:12 [in Sorting]
l:125 [in Indprop2]
l:129 [in Indprop2]
l:13 [in Higherorder]
l:130 [in Indprop2]
l:132 [in Indprop2]
l:14 [in Sorting]
l:16 [in Higherorder]
l:16 [in Sorting]
l:17 [in Sorting2]
l:18 [in Sorting]
l:19 [in Structures]
l:19 [in Sets]
l:19 [in Sorting]
l:2 [in Sets]
l:2 [in Sorting]
l:20 [in Higherorder]
l:23 [in Structures]
l:23 [in Sets]
l:29 [in Induction2]
l:3 [in Higherorder]
l:30 [in Higherorder]
l:34 [in Higherorder]
l:38 [in Lists]
l:39 [in Sorting2]
l:4 [in Structures]
l:4 [in Trees]
l:4 [in Sorting]
l:41 [in Higherorder]
l:43 [in Sorting2]
l:46 [in Sorting2]
l:47 [in Higherorder]
l:48 [in Induction]
l:49 [in Sorting2]
l:5 [in Sorting2]
l:5 [in Structures]
l:5 [in Sets]
l:52 [in Higherorder]
l:52 [in Induction]
l:54 [in Structures]
l:55 [in Indprop2]
l:57 [in Sorting2]
l:57 [in Structures]
l:58 [in Indprop2]
l:59 [in Structures]
l:6 [in Sorting]
l:61 [in Higherorder]
l:62 [in Sorting2]
l:65 [in Indprop2]
l:66 [in Induction]
l:67 [in Indprop]
l:7 [in Higherorder]
l:70 [in Indprop2]
l:70 [in Induction]
l:72 [in Sorting2]
l:73 [in Indprop]
l:74 [in Indprop2]
l:74 [in Induction]
l:75 [in Sorting2]
l:76 [in Indprop]
l:8 [in Higherorder]
l:8 [in Sets]
l:8 [in Sorting]
l:80 [in Indprop2]
l:81 [in Indprop]
l:83 [in Higherorder]
l:83 [in Sorting2]
l:83 [in Cases]
l:86 [in Indprop2]
l:86 [in Sorting2]
l:89 [in Higherorder]
l:9 [in Higherorder]
l:9 [in Sorting]
l:91 [in Sorting2]
l:92 [in Sorting2]
l:93 [in Higherorder]
l:93 [in Cases]
l:94 [in Sorting2]
l:95 [in Indprop2]
l:95 [in Sorting2]
l:95 [in Indprop]
l:96 [in Sorting2]
l:97 [in Sorting2]
l:98 [in Higherorder]
M
m:1 [in Indprop2]m:10 [in Indprop2]
m:10 [in Recursion]
m:101 [in Cases]
m:11 [in Induction2]
m:114 [in Indprop]
m:118 [in Indprop]
m:12 [in Indprop2]
m:122 [in Indprop]
m:133 [in Cases]
m:139 [in Cases]
m:14 [in Indprop2]
m:15 [in Recursion]
m:16 [in Indprop2]
m:17 [in Induction2]
m:170 [in Cases]
m:173 [in Cases]
m:19 [in Induction2]
m:19 [in Indprop]
m:2 [in Propositions]
m:2 [in Induction2]
m:2 [in Recursion]
m:2 [in Cases]
m:20 [in Induction]
m:21 [in Indprop2]
m:21 [in Induction2]
m:21 [in Recursion]
m:23 [in Indprop2]
m:24 [in Induction2]
m:25 [in Indprop2]
m:26 [in Induction2]
m:27 [in Indprop2]
m:27 [in Induction]
m:27 [in Trees]
m:29 [in Indprop2]
m:29 [in Cases]
m:29 [in Types]
m:30 [in Induction]
m:32 [in Indprop2]
m:32 [in Cases]
m:32 [in Exists]
m:33 [in Indprop]
m:33 [in Cases]
m:34 [in Cases]
m:34 [in Exists]
m:35 [in Indprop]
m:35 [in Types]
m:37 [in Indprop]
m:38 [in Types]
m:39 [in Indprop2]
m:39 [in Propositions]
m:4 [in Induction2]
m:4 [in Exists]
m:41 [in Propositions]
m:43 [in Induction]
m:43 [in Indprop]
m:44 [in Propositions]
m:45 [in Sets]
m:46 [in Propositions]
m:46 [in Indprop]
m:48 [in Propositions]
m:49 [in Induction]
m:49 [in Cases]
m:5 [in Induction]
m:5 [in Cases]
m:51 [in Cases]
m:52 [in Propositions]
m:53 [in Cases]
m:58 [in Propositions]
m:6 [in Indprop2]
m:6 [in Recursion]
m:7 [in Induction]
m:7 [in Cases]
m:70 [in Cases]
m:71 [in Propositions]
m:72 [in Cases]
m:74 [in Cases]
m:77 [in Cases]
m:8 [in Indprop2]
m:80 [in Induction]
m:82 [in Induction]
m:83 [in Structures]
m:85 [in Induction]
m:87 [in Induction]
m:88 [in Propositions]
m:88 [in Cases]
m:9 [in Induction]
m:9 [in Cases]
m:90 [in Induction]
N
n':11 [in Indprop]n':61 [in Indprop2]
n1:12 [in Induction2]
n1:143 [in Cases]
n1:159 [in Cases]
n1:19 [in Indprop2]
n1:33 [in Indprop2]
n1:36 [in Indprop2]
n1:39 [in Types]
n1:41 [in Types]
n1:44 [in Types]
n2:13 [in Induction2]
n2:144 [in Cases]
n2:160 [in Cases]
n2:20 [in Indprop2]
n2:34 [in Indprop2]
n2:37 [in Indprop2]
n2:40 [in Types]
n2:42 [in Types]
n2:45 [in Types]
n3:145 [in Cases]
n3:161 [in Cases]
n3:35 [in Indprop2]
n3:38 [in Indprop2]
n3:43 [in Types]
n3:46 [in Types]
n:1 [in Propositions]
n:1 [in Induction2]
n:1 [in Recursion]
n:1 [in Induction]
n:1 [in Cases]
n:1 [in Exists]
n:10 [in Induction2]
n:10 [in Indprop]
n:100 [in Cases]
n:101 [in Induction]
n:101 [in Structures]
n:11 [in Indprop2]
n:11 [in Induction]
n:11 [in Cases]
n:115 [in Indprop]
n:119 [in Indprop]
n:12 [in Propositions]
n:12 [in Induction]
n:12 [in Indprop]
n:12 [in Cases]
n:123 [in Indprop]
n:13 [in Indprop2]
n:13 [in Propositions]
n:13 [in Indprop]
n:13 [in Sorting]
n:132 [in Cases]
n:135 [in Cases]
n:136 [in Cases]
n:137 [in Cases]
n:138 [in Cases]
n:14 [in Propositions]
n:14 [in Recursion]
n:14 [in Indprop]
n:15 [in Indprop2]
n:15 [in Propositions]
n:15 [in Induction]
n:15 [in Indprop]
n:16 [in Induction2]
n:16 [in Induction]
n:16 [in Indprop]
n:16 [in Types]
n:167 [in Cases]
n:168 [in Cases]
n:169 [in Cases]
n:17 [in Induction]
n:17 [in Indprop]
n:171 [in Cases]
n:172 [in Cases]
n:18 [in Induction2]
n:18 [in Recursion]
n:18 [in Indprop]
n:19 [in Induction]
n:19 [in Exists]
n:2 [in Indprop2]
n:2 [in Induction]
n:2 [in Exists]
n:20 [in Induction2]
n:20 [in Recursion]
n:20 [in Types]
n:21 [in Indprop]
n:21 [in Exists]
n:22 [in Indprop2]
n:22 [in Induction]
n:22 [in Indprop]
n:22 [in Cases]
n:22 [in Types]
n:23 [in Induction2]
n:23 [in Induction]
n:23 [in Cases]
n:23 [in Exists]
n:24 [in Indprop2]
n:24 [in Higherorder]
n:24 [in Recursion]
n:24 [in Types]
n:25 [in Induction2]
n:25 [in Exists]
n:26 [in Indprop2]
n:26 [in Recursion]
n:26 [in Induction]
n:26 [in Trees]
n:27 [in Induction2]
n:27 [in Types]
n:28 [in Indprop2]
n:28 [in Indprop]
n:28 [in Types]
n:29 [in Recursion]
n:29 [in Induction]
n:29 [in Expressions]
n:3 [in Induction2]
n:3 [in Induction]
n:3 [in Structures]
n:3 [in Indprop]
n:3 [in Cases]
n:3 [in Expressions]
n:30 [in Indprop]
n:31 [in Indprop2]
n:31 [in Recursion]
n:31 [in Trees]
n:31 [in Exists]
n:32 [in Induction]
n:32 [in Indprop]
n:33 [in Exists]
n:34 [in Indprop]
n:34 [in Types]
n:35 [in Recursion]
n:35 [in Cases]
n:35 [in Trees]
n:36 [in Recursion]
n:36 [in Indprop]
n:36 [in Expressions]
n:37 [in Types]
n:38 [in Propositions]
n:38 [in Cases]
n:4 [in Indprop2]
n:4 [in Propositions]
n:4 [in Induction]
n:4 [in Cases]
n:40 [in Propositions]
n:40 [in Trees]
n:41 [in Indprop]
n:41 [in Sets]
n:42 [in Induction]
n:42 [in Indprop]
n:43 [in Propositions]
n:43 [in Higherorder]
n:43 [in Sets]
n:45 [in Propositions]
n:45 [in Indprop]
n:47 [in Propositions]
n:48 [in Cases]
n:48 [in Types]
n:49 [in Indprop]
n:49 [in Types]
n:5 [in Indprop2]
n:5 [in Propositions]
n:5 [in Recursion]
n:5 [in Indprop]
n:50 [in Induction]
n:50 [in Sets]
n:50 [in Cases]
n:50 [in Types]
n:51 [in Propositions]
n:51 [in Types]
n:52 [in Indprop]
n:52 [in Cases]
n:55 [in Indprop]
n:57 [in Propositions]
n:57 [in Indprop]
n:58 [in Cases]
n:6 [in Propositions]
n:6 [in Induction]
n:6 [in Cases]
n:60 [in Indprop2]
n:60 [in Types]
n:61 [in Propositions]
n:61 [in Sorting2]
n:61 [in Structures]
n:61 [in Types]
n:62 [in Propositions]
n:64 [in Indprop]
n:68 [in Indprop]
n:69 [in Cases]
n:7 [in Indprop2]
n:70 [in Propositions]
n:71 [in Cases]
n:72 [in Expressions]
n:73 [in Cases]
n:76 [in Cases]
n:79 [in Induction]
n:8 [in Induction]
n:8 [in Indprop]
n:8 [in Cases]
n:82 [in Sorting2]
n:82 [in Structures]
n:83 [in Induction]
n:84 [in Induction]
n:85 [in Propositions]
n:85 [in Indprop]
n:85 [in Cases]
n:86 [in Cases]
n:87 [in Propositions]
n:87 [in Cases]
n:89 [in Indprop]
n:9 [in Indprop2]
n:9 [in Recursion]
n:9 [in Indprop]
n:93 [in Induction]
O
OkType:153 [in Structures]opt:108 [in Structures]
opt:113 [in Structures]
opt:117 [in Structures]
opt:121 [in Structures]
or:72 [in Higherorder]
other:50 [in Indprop2]
out:91 [in Higherorder]
out:95 [in Higherorder]
ox:127 [in Structures]
oy:128 [in Structures]
o1:123 [in Structures]
o1:131 [in Structures]
o1:137 [in Structures]
o1:148 [in Cases]
o1:156 [in Cases]
o1:164 [in Cases]
o1:42 [in Indprop2]
o1:47 [in Indprop2]
o1:56 [in Types]
o1:63 [in Types]
o1:70 [in Types]
o2:124 [in Structures]
o2:132 [in Structures]
o2:138 [in Structures]
o2:149 [in Cases]
o2:157 [in Cases]
o2:165 [in Cases]
o2:43 [in Indprop2]
o2:48 [in Indprop2]
o2:57 [in Types]
o2:64 [in Types]
o2:71 [in Types]
o3:139 [in Structures]
o3:150 [in Cases]
o3:158 [in Cases]
o3:166 [in Cases]
o3:44 [in Indprop2]
o3:49 [in Indprop2]
o3:65 [in Types]
o3:72 [in Types]
o:10 [in Cases]
o:116 [in Indprop]
o:120 [in Indprop]
o:124 [in Indprop]
o:20 [in Indprop]
o:3 [in Indprop2]
o:3 [in Exists]
o:30 [in Indprop2]
o:42 [in Propositions]
o:49 [in Propositions]
o:53 [in Propositions]
o:71 [in Higherorder]
o:72 [in Propositions]
o:75 [in Cases]
o:78 [in Cases]
o:89 [in Propositions]
P
pair:80 [in Structures]pair:81 [in Structures]
path:161 [in Structures]
prog:79 [in Expressions]
prog:84 [in Expressions]
p:10 [in Induction]
P:10 [in Exists]
P:101 [in Sorting2]
P:104 [in Cases]
P:106 [in Cases]
P:108 [in Cases]
P:109 [in Cases]
P:114 [in Cases]
P:128 [in Cases]
P:14 [in Exists]
P:17 [in Propositions]
P:19 [in Propositions]
p:21 [in Induction]
p:22 [in Induction2]
p:24 [in Sorting]
p:27 [in Sorting]
P:28 [in Propositions]
p:28 [in Induction]
P:28 [in Exists]
P:29 [in Exists]
p:31 [in Induction]
P:34 [in Propositions]
P:36 [in Exists]
p:38 [in Indprop]
P:39 [in Cases]
P:40 [in Exists]
P:41 [in Cases]
P:43 [in Cases]
P:45 [in Cases]
p:5 [in Types]
p:50 [in Propositions]
p:54 [in Propositions]
P:54 [in Cases]
P:56 [in Cases]
P:59 [in Cases]
P:6 [in Exists]
P:60 [in Cases]
P:61 [in Cases]
P:63 [in Cases]
P:64 [in Cases]
p:71 [in Structures]
p:75 [in Structures]
p:81 [in Induction]
p:86 [in Induction]
p:87 [in Sorting2]
p:89 [in Sorting2]
p:90 [in Propositions]
P:92 [in Indprop2]
P:93 [in Indprop2]
p:94 [in Structures]
P:97 [in Cases]
P:99 [in Indprop2]
P:99 [in Cases]
Q
Q:105 [in Cases]Q:107 [in Cases]
Q:110 [in Cases]
Q:115 [in Cases]
Q:15 [in Exists]
Q:18 [in Propositions]
Q:20 [in Propositions]
Q:29 [in Propositions]
Q:35 [in Propositions]
Q:40 [in Cases]
Q:42 [in Cases]
Q:44 [in Cases]
Q:46 [in Cases]
q:55 [in Propositions]
Q:55 [in Cases]
Q:57 [in Cases]
q:59 [in Propositions]
Q:62 [in Cases]
Q:65 [in Cases]
Q:98 [in Cases]
R
R:111 [in Cases]R:116 [in Cases]
r:164 [in Structures]
r:170 [in Structures]
r:173 [in Structures]
r:178 [in Structures]
R:21 [in Propositions]
R:47 [in Cases]
r:56 [in Propositions]
r:6 [in Trees]
r:60 [in Propositions]
r:74 [in Indprop]
r:77 [in Indprop]
r:82 [in Indprop]
r:97 [in Indprop]
S
seed:51 [in Higherorder]seed:60 [in Higherorder]
stack:75 [in Expressions]
stack:78 [in Expressions]
stack:83 [in Expressions]
stack:86 [in Expressions]
st:27 [in Expressions]
st:30 [in Expressions]
st:53 [in Expressions]
st:57 [in Expressions]
st:74 [in Expressions]
st:77 [in Expressions]
st:82 [in Expressions]
s:42 [in Sets]
s:44 [in Sets]
s:51 [in Sets]
T
test:103 [in Indprop2]test:108 [in Indprop2]
test:12 [in Higherorder]
test:2 [in Higherorder]
t':33 [in Sorting2]
t1:37 [in Sets]
t1:46 [in Sets]
t1:48 [in Sets]
t2:38 [in Sets]
t2:47 [in Sets]
t2:49 [in Sets]
t:103 [in Indprop]
t:107 [in Indprop]
t:11 [in Trees]
t:13 [in Trees]
t:16 [in Trees]
t:21 [in Trees]
t:32 [in Trees]
t:36 [in Trees]
t:38 [in Trees]
t:41 [in Trees]
t:57 [in Induction]
t:61 [in Induction]
t:63 [in Indprop]
t:8 [in Trees]
t:86 [in Indprop]
T:89 [in Indprop2]
t:90 [in Indprop]
t:94 [in Indprop2]
T:98 [in Indprop2]
V
v:19 [in Trees]v:5 [in Trees]
v:78 [in Indprop]
v:83 [in Indprop]
v:96 [in Indprop]
X
X:1 [in Higherorder]x:1 [in Sets]
X:1 [in Trees]
x:10 [in Propositions]
X:10 [in Trees]
x:101 [in Indprop2]
X:101 [in Indprop]
X:102 [in Indprop2]
X:102 [in Higherorder]
X:104 [in Structures]
x:105 [in Higherorder]
x:106 [in Higherorder]
X:106 [in Structures]
X:107 [in Indprop2]
X:107 [in Structures]
X:11 [in Higherorder]
x:11 [in Exists]
x:110 [in Indprop2]
X:110 [in Structures]
X:114 [in Structures]
X:118 [in Structures]
X:12 [in Trees]
x:12 [in Exists]
X:122 [in Structures]
x:124 [in Indprop2]
X:125 [in Structures]
x:128 [in Indprop2]
X:13 [in Exists]
x:131 [in Indprop2]
x:14 [in Induction2]
x:14 [in Higherorder]
X:143 [in Structures]
x:146 [in Structures]
x:149 [in Structures]
X:15 [in Higherorder]
X:15 [in Structures]
X:15 [in Trees]
x:157 [in Structures]
x:158 [in Structures]
x:16 [in Exists]
X:162 [in Structures]
X:166 [in Structures]
X:17 [in Higherorder]
x:17 [in Exists]
X:171 [in Structures]
X:174 [in Structures]
x:18 [in Structures]
X:18 [in Trees]
x:18 [in Exists]
X:20 [in Structures]
X:20 [in Trees]
X:21 [in Structures]
X:22 [in Structures]
x:22 [in Sets]
x:23 [in Higherorder]
x:25 [in Sorting]
X:26 [in Structures]
X:27 [in Higherorder]
x:27 [in Structures]
X:28 [in Induction2]
x:28 [in Cases]
x:28 [in Expressions]
x:28 [in Sorting]
X:29 [in Lists]
x:30 [in Cases]
X:31 [in Structures]
x:31 [in Expressions]
X:32 [in Higherorder]
x:32 [in Structures]
x:33 [in Induction]
X:35 [in Exists]
x:36 [in Higherorder]
x:36 [in Induction]
X:36 [in Structures]
X:36 [in Lists]
x:37 [in Higherorder]
X:37 [in Structures]
x:37 [in Expressions]
x:37 [in Exists]
X:38 [in Higherorder]
X:38 [in Structures]
x:38 [in Exists]
x:39 [in Induction]
x:39 [in Structures]
X:39 [in Exists]
x:4 [in Sorting2]
x:41 [in Sorting2]
x:41 [in Exists]
x:42 [in Exists]
X:43 [in Structures]
X:44 [in Higherorder]
x:44 [in Structures]
X:48 [in Higherorder]
X:48 [in Structures]
X:5 [in Exists]
X:51 [in Induction]
X:53 [in Induction]
X:53 [in Structures]
x:54 [in Indprop2]
x:54 [in Sorting2]
x:55 [in Higherorder]
x:55 [in Sorting2]
x:56 [in Indprop2]
X:56 [in Induction]
X:57 [in Higherorder]
X:59 [in Indprop]
X:6 [in Higherorder]
X:60 [in Sorting2]
X:60 [in Induction]
X:62 [in Induction]
X:62 [in Structures]
X:63 [in Structures]
x:64 [in Higherorder]
X:65 [in Induction]
x:66 [in Indprop2]
X:66 [in Indprop]
x:67 [in Higherorder]
x:67 [in Structures]
x:68 [in Cases]
X:69 [in Propositions]
X:69 [in Structures]
X:69 [in Indprop]
x:7 [in Sets]
X:7 [in Trees]
x:7 [in Exists]
X:70 [in Higherorder]
X:71 [in Induction]
x:72 [in Indprop2]
x:72 [in Indprop]
X:73 [in Structures]
x:73 [in Expressions]
x:73 [in Types]
x:74 [in Higherorder]
x:75 [in Indprop]
X:76 [in Higherorder]
x:76 [in Structures]
x:76 [in Types]
X:77 [in Indprop2]
x:78 [in Higherorder]
X:78 [in Structures]
x:78 [in Types]
x:79 [in Higherorder]
x:79 [in Sorting2]
X:79 [in Cases]
x:8 [in Induction2]
x:8 [in Sorting2]
x:8 [in Exists]
x:80 [in Indprop]
x:80 [in Cases]
X:81 [in Higherorder]
x:84 [in Higherorder]
x:84 [in Sorting2]
X:84 [in Structures]
X:86 [in Higherorder]
x:88 [in Indprop2]
x:88 [in Sorting2]
x:88 [in Structures]
X:89 [in Cases]
X:9 [in Exists]
x:90 [in Higherorder]
x:90 [in Sorting2]
X:90 [in Structures]
x:90 [in Cases]
X:92 [in Higherorder]
x:94 [in Higherorder]
X:95 [in Structures]
X:96 [in Higherorder]
x:98 [in Structures]
X:99 [in Higherorder]
X:99 [in Structures]
Y
y1:147 [in Structures]y2:148 [in Structures]
y:11 [in Propositions]
Y:111 [in Structures]
Y:115 [in Structures]
Y:119 [in Structures]
Y:126 [in Structures]
Y:144 [in Structures]
y:15 [in Induction2]
Y:167 [in Structures]
Y:18 [in Higherorder]
y:26 [in Sorting]
Y:28 [in Higherorder]
y:29 [in Sorting]
Y:30 [in Lists]
y:34 [in Induction]
y:37 [in Induction]
Y:37 [in Lists]
Y:39 [in Higherorder]
y:40 [in Induction]
Y:45 [in Higherorder]
Y:49 [in Higherorder]
y:56 [in Higherorder]
y:56 [in Sorting2]
y:57 [in Indprop2]
Y:58 [in Higherorder]
Y:64 [in Structures]
y:68 [in Structures]
Y:70 [in Structures]
y:71 [in Indprop2]
Y:72 [in Induction]
Y:74 [in Structures]
y:77 [in Structures]
Y:78 [in Indprop2]
Y:79 [in Structures]
y:80 [in Sorting2]
y:81 [in Cases]
y:85 [in Sorting2]
Y:85 [in Structures]
y:87 [in Indprop2]
Y:87 [in Higherorder]
y:89 [in Structures]
y:9 [in Induction2]
y:9 [in Sorting2]
Y:91 [in Structures]
y:91 [in Cases]
Z
z:35 [in Induction]z:38 [in Induction]
z:41 [in Induction]
z:82 [in Cases]
Z:86 [in Structures]
Z:92 [in Structures]
z:92 [in Cases]
_
_n:40 [in Sets]Module Index
A
AExp [in Expressions]B
BSTSets [in Sets]D
DefnFixpoint [in Recursion]E
Errors [in Structures]Errors.BadErrors [in Structures]
F
FunSets [in Sets]M
MonoList [in Structures]MyIff [in Cases]
MyNot [in Cases]
N
NatPlayground [in Types]NatPlayground2 [in Recursion]
O
OptionPlayground [in Structures]P
PairProjection [in Structures]Playground [in Indprop]
R
R [in Indprop]S
SortedSets [in Sets]Library Index
C
CasesE
ExistsExpressions
H
HigherorderI
IndpropIndprop2
Induction
Induction2
Intro
L
ListsP
PostscriptPreface
Propositions
R
RecursionS
SetsSorting
Sorting2
Structures
T
TreesTypes
Lemma Index
A
addn_preserves_sortedness [in Sorting2]add1_preserves_sortedness [in Sorting2]
add2_preserves_sortedness [in Sorting2]
All_In [in Indprop2]
All_nth [in Sorting2]
All_perm [in Sorting2]
all3_spec [in Induction]
andb_false_r [in Induction]
andb_true_iff [in Cases]
andb_true_elim2 [in Cases]
andb_commutative'' [in Cases]
andb_commutative' [in Cases]
andb_commutative [in Cases]
andb3_exchange [in Cases]
and_PQ [in Propositions]
and_intro_sloppy [in Propositions]
and_intro_braces [in Propositions]
and_intro [in Propositions]
and_example2'' [in Cases]
and_example2' [in Cases]
and_example2 [in Cases]
and_assoc [in Cases]
and_commut [in Cases]
apply_iff_example [in Cases]
app_length [in Induction]
app_nil_r [in Induction]
app_assoc [in Induction]
argmin3_leb [in Indprop2]
argmin3_min [in Indprop2]
argmin3_min3 [in Cases]
argmin3_min3_eqs [in Cases]
assumed_A [in Propositions]
B
bad_function_breaks_sortedness [in Sorting2]bin_nat_bin [in Induction]
btbase__not_found [in Indprop]
btx__nat_in_tree [in Indprop]
C
complementary_complementary' [in Induction2]complement_correct [in Induction2]
complement_involutive [in Cases]
contradiction_implies_anything [in Cases]
contrapositive [in Cases]
D
discriminate_ex2 [in Cases]discriminate_ex1 [in Cases]
dist_exists_or [in Exists]
dist_not_forall [in Exists]
dist_not_exists [in Exists]
double_injective_take2 [in Induction2]
double_injective_take2_FAILED [in Induction2]
double_injective [in Induction2]
double_injective_FAILED [in Induction2]
double_plus [in Induction]
double_neg [in Cases]
E
eqb_trans [in Induction2]eqb_sym [in Induction2]
eqb_false_iff [in Induction2]
eqb_true_iff [in Induction2]
eqb_true [in Induction2]
eqb_refl [in Induction]
eqb_0_l [in Cases]
eq_strand_iff [in Induction2]
eq_strand_refl [in Induction]
eq_base_iff [in Cases]
eq_base_true [in Cases]
eq_base_refl [in Cases]
evenb_double_conv [in Exists]
evenb_double [in Exists]
evenb_S [in Exists]
even_bool_prop [in Exists]
everywhere_perm [in Sorting2]
evSS_ev'_subst [in Indprop]
evSS_ev' [in Indprop]
evSS_ev [in Indprop]
evSS_ev [in Indprop]
ev_plus_plus [in Indprop]
ev_ev__ev [in Indprop]
ev_sum [in Indprop]
ev_even_iff [in Indprop]
ev_even [in Indprop]
ev_even_firsttry [in Indprop]
ev_minus2 [in Indprop]
ev_inversion [in Indprop]
ev_double [in Indprop]
ev_plus4 [in Indprop]
ev_4' [in Indprop]
ev_4 [in Indprop]
ev5_nonsense [in Indprop]
exists_example_2 [in Exists]
ex_falso_quodlibet [in Cases]
F
filter_preserves_sortedness [in Sorting2]forallb_true_iff [in Indprop2]
four_is_even [in Exists]
funny_rec_evenb_0 [in Cases]
f_equal [in Induction2]
I
identity_fn_applied_twice [in Cases]iff_trans [in Cases]
iff_refl [in Cases]
iff_sym [in Cases]
implies_PQR [in Propositions]
injection_discriminate [in Cases]
injection_ex2 [in Cases]
injection_ex1 [in Cases]
insertion_sort_correct [in Sorting2]
insert_preserves_setlike [in Indprop2]
insert_sorted_sorted' [in Sorting2]
insert_sorted_sorted [in Sorting2]
insert_sorted_perm [in Sorting2]
inversion_ex2 [in Indprop]
inversion_ex1 [in Indprop]
In_member_iff [in Indprop2]
In_flat_map [in Indprop2]
In_app_iff [in Indprop2]
In_map_iff [in Indprop2]
In_map [in Indprop2]
is_setlike__setlike [in Indprop2]
is_sorted_iff_sorted [in Sorting2]
L
leb_iff [in Indprop2]leb_true_trans [in Indprop2]
leb_correct [in Indprop2]
leb_complete [in Indprop2]
leb_nm__leb_mn' [in Indprop2]
leb_spec [in Indprop2]
leb_nm__leb_mn [in Indprop2]
leb_refl [in Induction]
le_plus_l [in Indprop2]
le_trans [in Indprop2]
listnum_iff [in Indprop]
lt_S [in Indprop2]
M
map_rev [in Induction]map_length [in Induction]
minus_Sn_m [in Indprop2]
minus_Sn_n [in Induction]
minus_diag [in Induction]
minus_n_O [in Cases]
min3_leb [in Indprop2]
min3_min [in Indprop2]
modus_ponens [in Propositions]
monotonic_preserves_sortedness [in Sorting2]
mult_S_1 [in Propositions]
mult_0_plus [in Propositions]
mult_0_l [in Propositions]
mult_comm [in Induction]
mult_assoc [in Induction]
mult_plus_distr_r [in Induction]
mult_1_l [in Induction]
mult_0_r [in Induction]
mult_0_plus' [in Cases]
N
nat_bin_nat [in Induction]negb_involutive [in Cases]
not_P__P_true [in Cases]
not_true_iff_false [in Cases]
not_both_true_and_false [in Cases]
not_true_is_false' [in Cases]
not_true_is_false [in Cases]
not_implies_our_not [in Cases]
not_False [in Cases]
not_forall__exists_not [in Exists]
not_exists__forall_not [in Exists]
nth_error_after_last [in Induction2]
n_le_m__Sn_le_Sm [in Indprop2]
O
one_not_even' [in Indprop]one_not_even [in Indprop]
orb_true [in Induction]
orb_true_3 [in Cases]
orb_true_iff [in Cases]
or_which [in Propositions]
or_inclusive2 [in Propositions]
or_inclusive1 [in Propositions]
or_intro_r [in Propositions]
or_intro_l [in Propositions]
or_assoc [in Cases]
or_commut' [in Cases]
or_commut [in Cases]
O_le_n [in Indprop2]
P
permutations_complete [in Sorting2]Permutation_sym [in Sorting2]
Permutation_length [in Sorting2]
Permutation_refl [in Sorting2]
Playground.test_le3 [in Indprop]
Playground.test_le2 [in Indprop]
Playground.test_le1 [in Indprop]
plus_lt [in Indprop2]
plus_id_exercise [in Propositions]
plus_id_example [in Propositions]
plus_1_l [in Propositions]
plus_O_n' [in Propositions]
plus_O_n [in Propositions]
plus_n_Sm [in Induction2]
plus_swap' [in Induction]
plus_swap [in Induction]
plus_comm3_take3 [in Induction]
plus_comm3_take2 [in Induction]
plus_comm3 [in Induction]
plus_ble_compat_l [in Induction]
plus_assoc [in Induction]
plus_comm [in Induction]
plus_n_Sm [in Induction]
plus_n_O [in Induction]
plus_1_neq_0' [in Cases]
plus_1_neq_0 [in Cases]
plus_1_neq_0_firsttry [in Cases]
proj1 [in Cases]
proj2 [in Cases]
R
restricted_excluded_middle_eq [in Exists]restricted_excluded_middle [in Exists]
rev_involutive [in Induction]
rev_app_distr [in Induction]
R.R_equiv_fR [in Indprop]
S
sillyfun_false [in Cases]sillyfun1_odd [in Cases]
sillyfun1_odd_FAILED [in Cases]
silly_ex [in Propositions]
silly_fact_2' [in Cases]
silly_fact_2 [in Cases]
silly_fact_2_FAILED [in Cases]
silly_fact_1 [in Cases]
silly1 [in Propositions]
silly2 [in Propositions]
silly2a [in Propositions]
silly3_firsttry [in Propositions]
silly3' [in Cases]
size_length_inorder [in Induction]
Sn_le_Sm__n_le_m [in Indprop2]
sorted_sorted' [in Sorting2]
sorted_filter_cons [in Sorting2]
sorted_smaller [in Sorting2]
sorted'_sorted [in Sorting2]
sort_sorted' [in Sorting2]
sort_idempotent [in Sorting2]
sort_already_sorted [in Sorting2]
sort_sorted [in Sorting2]
sort_perm [in Sorting2]
square_mult [in Cases]
SSSSev__even [in Indprop]
S_nbeq_0 [in Induction]
S_inj [in Cases]
S_injective' [in Cases]
S_injective [in Cases]
T
trans_eq [in Propositions]True_or_r [in Propositions]
True_or_l [in Propositions]
True_and_id [in Propositions]
True_is_true' [in Propositions]
True_is_true [in Propositions]
U
union_intersection_dist [in Indprop2]union_preserves_setlike [in Indprop2]
Z
zero_nbeq_S [in Induction]zero_not_one' [in Cases]
zero_not_one [in Cases]
zero_or_succ [in Cases]
Constructor Index
A
A [in Intro]AExp.AMinus [in Expressions]
AExp.AMult [in Expressions]
AExp.ANum [in Expressions]
AExp.APlus [in Expressions]
AExp.BAnd [in Expressions]
AExp.BEq [in Expressions]
AExp.BFalse [in Expressions]
AExp.BLe [in Expressions]
AExp.BNot [in Expressions]
AExp.BTrue [in Expressions]
AId [in Expressions]
Ala [in Lists]
All_cons [in Indprop2]
All_nil [in Indprop2]
AMinus [in Expressions]
AMult [in Expressions]
ANum [in Expressions]
APlus [in Expressions]
Arg [in Lists]
Asn [in Lists]
Asp [in Lists]
B
BAnd [in Expressions]bb_node [in Indprop]
bb_empty [in Indprop]
BEq [in Expressions]
BFalse [in Expressions]
black [in Types]
BLe [in Expressions]
blue [in Types]
BNot [in Expressions]
BTrue [in Expressions]
bx_right [in Indprop]
bx_left [in Indprop]
bx_found [in Indprop]
BZ [in Recursion]
C
C [in Intro]cons [in Structures]
Cys [in Lists]
E
empty [in Trees]EQ [in Trees]
Errors.BadErrors.file_not_found [in Structures]
Errors.BadErrors.ok [in Structures]
Errors.BadErrors.operation_canceled [in Structures]
Errors.BadErrors.permission_denied [in Structures]
Errors.BadErrors.temporarily_unavailable [in Structures]
Errors.Error [in Structures]
Errors.file_not_found [in Structures]
Errors.Ok [in Structures]
Errors.operation_canceled [in Structures]
Errors.permission_denied [in Structures]
Errors.temporarily_unavailable [in Structures]
ev_SS [in Indprop]
ev_0 [in Indprop]
F
false [in Intro]friday [in Intro]
G
G [in Intro]Gln [in Lists]
Glu [in Lists]
Gly [in Lists]
green [in Types]
GT [in Trees]
H
His [in Lists]I
Ile [in Lists]In_cons [in Indprop2]
In_here [in Indprop2]
L
Leu [in Lists]ln_cons [in Indprop]
ln_nil [in Indprop]
LT [in Trees]
Lys [in Lists]
M
Met [in Lists]monday [in Intro]
MonoList.bool_cons [in Structures]
MonoList.bool_nil [in Structures]
MonoList.nat_cons [in Structures]
MonoList.nat_nil [in Structures]
N
NatPlayground.O [in Types]NatPlayground.S [in Types]
NatPlayground.stop [in Types]
NatPlayground.tick [in Types]
ne_2 [in Indprop]
ne_1 [in Indprop]
nil [in Structures]
nn [in Indprop]
node [in Trees]
O
OptionPlayground.None [in Structures]OptionPlayground.Some [in Structures]
P
pair [in Structures]perm_trans [in Sorting2]
perm_swap [in Sorting2]
perm_skip [in Sorting2]
perm_nil [in Sorting2]
Phe [in Lists]
Playground.le_S [in Indprop]
Playground.le_n [in Indprop]
primary [in Types]
Pro [in Lists]
R
red [in Types]R.c1 [in Indprop]
R.c2 [in Indprop]
R.c3 [in Indprop]
S
saturday [in Intro]Ser [in Lists]
setlike_cons [in Indprop2]
setlike_nil [in Indprop2]
SLoad [in Expressions]
SMinus [in Expressions]
SMult [in Expressions]
sorted_cons [in Sorting2]
sorted_1 [in Sorting2]
sorted_nil [in Sorting2]
SPlus [in Expressions]
SPush [in Expressions]
sq [in Indprop]
STOP [in Lists]
sunday [in Intro]
T
T [in Intro]Thr [in Lists]
thursday [in Intro]
Trp [in Lists]
true [in Intro]
tuesday [in Intro]
Tyr [in Lists]
T2 [in Recursion]
T2P1 [in Recursion]
V
Val [in Lists]W
wednesday [in Intro]white [in Types]
wrong_ev_SS [in Indprop]
wrong_ev_0 [in Indprop]
Inductive Index
A
aexp [in Expressions]AExp.aexp [in Expressions]
AExp.bexp [in Expressions]
All [in Indprop2]
B
base [in Intro]bexp [in Expressions]
bin [in Recursion]
bool [in Intro]
bt [in Trees]
btbase [in Indprop]
btx [in Indprop]
C
codon [in Lists]color [in Types]
D
day [in Intro]E
Errors.BadErrors.FileError_FirstTry [in Structures]Errors.FileError [in Structures]
Errors.result [in Structures]
ev [in Indprop]
I
In [in Indprop2]L
list [in Structures]listnum [in Indprop]
M
MonoList.boollist [in Structures]MonoList.natlist [in Structures]
N
NatPlayground.nat [in Types]NatPlayground.nat' [in Types]
next_ev [in Indprop]
next_nat [in Indprop]
O
OptionPlayground.option [in Structures]ordering [in Trees]
P
Permutation [in Sorting2]Playground.le [in Indprop]
prod [in Structures]
R
rgb [in Types]R.R [in Indprop]
S
setlike [in Indprop2]sinstr [in Expressions]
sorted [in Sorting2]
square_of [in Indprop]
W
wrong_ev [in Indprop]Definition Index
A
aeval [in Expressions]AExp.aeval [in Expressions]
AExp.beval [in Expressions]
AExp.optimize_0plus [in Expressions]
allb [in Structures]
andb [in Intro]
and_example' [in Propositions]
and_example [in Propositions]
and_option [in Structures]
and_then [in Structures]
app [in Structures]
argmin [in Structures]
argmin [in Types]
argmin3 [in Structures]
argmin3 [in Cases]
argmin3 [in Types]
argmin3' [in Types]
B
bad_function [in Sorting2]bar [in Cases]
beval [in Expressions]
bge [in Expressions]
bgt [in Expressions]
bin_to_nat [in Induction]
blt [in Expressions]
bne [in Expressions]
bor [in Expressions]
BSTSets.empty_natset [in Sets]
BSTSets.manual_grade_for_bst_set_definitions [in Sets]
BSTSets.natset [in Sets]
BSTSets.set_insert [in Sets]
BSTSets.union [in Sets]
bst1 [in Trees]
bst2 [in Trees]
b_eleven [in Recursion]
b_nine [in Recursion]
b_three [in Recursion]
b_two [in Recursion]
b_one [in Recursion]
b_zero [in Recursion]
C
combine [in Lists]compare [in Trees]
complement [in Intro]
complementary [in Lists]
complementary' [in Induction2]
complementary' [in Higherorder]
constfun [in Types]
const_empty_list [in Sorting]
countoddmembers' [in Higherorder]
D
DefnFixpoint.double [in Recursion]DefnFixpoint.pred [in Recursion]
different_all_three [in Trees]
discriminate_ex3 [in Cases]
double [in Induction]
double_bin [in Induction]
E
empty_natset [in Sets]empty_st [in Expressions]
encode [in Lists]
encode_one [in Lists]
enumerate [in Higherorder]
eqb [in Types]
eq_base [in Intro]
eq_strand [in Induction]
eq_strand [in Lists]
eq_base [in Lists]
Errors.read_file [in Structures]
Errors.result_or_else [in Structures]
Errors.result_transpose [in Structures]
Errors.result_map [in Structures]
Errors.result_to_option [in Structures]
evenb [in Types]
evens_to_ten' [in Sets]
evens_to_ten [in Sets]
even_1000'' [in Exists]
even_1000' [in Exists]
even_1000 [in Exists]
everywhere [in Sorting2]
excluded_middle [in Exists]
extend_st [in Expressions]
extra_zero [in Sorting]
F
factorial [in Recursion]favorite_day' [in Structures]
favorite_day [in Types]
fetch_st [in Expressions]
filter [in Higherorder]
filter_even_gt7 [in Higherorder]
filter' [in Higherorder]
first_satisfying [in Higherorder]
flat_map [in Indprop2]
flat_map' [in Higherorder]
flat_map [in Higherorder]
flip [in Types]
fold_left [in Higherorder]
fold_right [in Higherorder]
foo [in Cases]
forallb [in Indprop2]
forallb_bt [in Indprop]
funny_rec [in Cases]
FunSets.empty_natset [in Sets]
FunSets.intersection [in Sets]
FunSets.manual_grade_for_fun_subset [in Sets]
FunSets.manual_grade_for_fun_remove [in Sets]
FunSets.manual_grade_for_fun_operations [in Sets]
FunSets.member [in Sets]
FunSets.natset [in Sets]
FunSets.set_remove [in Sets]
FunSets.set_insert [in Sets]
FunSets.union [in Sets]
f7 [in Types]
H
half [in Recursion]hd_error [in Structures]
head_only [in Sorting]
I
id_list [in Sorting]ill_typed_sort [in Sorting]
impb [in Intro]
incr [in Induction]
injection_ex3 [in Cases]
injective [in Propositions]
inorder [in Trees]
insert [in Trees]
insert_sorted [in Sorting2]
insert_sorted [in Sorting]
intersection [in Indprop2]
intersection [in Sets]
In_example_2 [in Indprop2]
In_example_1 [in Indprop2]
isred [in Types]
isred' [in Types]
is_setlike [in Indprop2]
is_three [in Propositions]
is_sorted [in Sorting2]
is_a_sorting_algorithm [in Sorting2]
is_weekday [in Intro]
is_setlike [in Sets]
is_leaf [in Trees]
is_permutation_of [in Sorting]
is_sorted [in Sorting]
is_weekday' [in Types]
is_even_prime [in Exists]
L
leaf [in Trees]leb [in Cases]
leb [in Types]
lemma_application_ex2 [in Induction]
lemma_application_ex1 [in Induction]
length [in Structures]
length_is_1 [in Higherorder]
length' [in Higherorder]
list123 [in Structures]
list123 [in Lists]
list123' [in Structures]
list123' [in Lists]
list123'' [in Structures]
list123'' [in Lists]
list123''' [in Lists]
lookup [in Trees]
lt [in Indprop]
ltb [in Types]
l0 [in Sorting]
l1 [in Sorting]
l2 [in Sorting]
l3 [in Sorting]
l4 [in Sorting]
M
manual_grade_for_mult_S_1_informal [in Propositions]manual_grade_for_or_which_informal [in Propositions]
manual_grade_for_and_PQ_informal [in Propositions]
manual_grade_for_implies_PQR_informal [in Propositions]
manual_grade_for_mult_0_l_informal [in Propositions]
manual_grade_for_nth_error_after_last_informal [in Induction2]
manual_grade_for_fold_practice [in Higherorder]
manual_grade_for_is_classday [in Intro]
manual_grade_for_table [in Intro]
manual_grade_for_xorb [in Intro]
manual_grade_for_impb [in Intro]
manual_grade_for_nandb [in Intro]
manual_grade_for_normalize [in Recursion]
manual_grade_for_nat_to_bin [in Recursion]
manual_grade_for_binary [in Recursion]
manual_grade_for_decreasing [in Recursion]
manual_grade_for_double_plus_informal [in Induction]
manual_grade_for_option_map' [in Structures]
manual_grade_for_list_min [in Structures]
manual_grade_for_currying [in Structures]
manual_grade_for_forall_exists [in Lists]
manual_grade_for_sums_to [in Indprop]
manual_grade_for_ev_sum_informal [in Indprop]
manual_grade_for_set_equal [in Sets]
manual_grade_for_argmin3_min3_eqs_informal [in Cases]
manual_grade_for_injection_discriminate_informal [in Cases]
manual_grade_for_negation_fn_applied_twice [in Cases]
manual_grade_for_contrapositive_informal [in Cases]
manual_grade_for_zero_or_succ_informal [in Cases]
manual_grade_for_and_assoc_informal [in Cases]
manual_grade_for_negb_involutive_informal [in Cases]
manual_grade_for_encodings [in Expressions]
manual_grade_for_is_bst [in Trees]
manual_grade_for_search_property [in Trees]
manual_grade_for_traversals [in Trees]
manual_grade_for_partial_app_minus [in Types]
manual_grade_for_mirror [in Types]
manual_grade_for_ltb [in Types]
manual_grade_for_test_leb [in Types]
map [in Higherorder]
map_option' [in Higherorder]
map_option [in Higherorder]
map' [in Higherorder]
member [in Sets]
min [in Types]
minustwo [in Propositions]
minustwo [in Types]
min_by' [in Higherorder]
min_by [in Higherorder]
min3 [in Cases]
min3 [in Types]
min3' [in Types]
mirror' [in Types]
monochrome [in Types]
MonoList.boollist_length [in Structures]
MonoList.natlist_length [in Structures]
monotonic [in Sorting2]
MyIff.iff [in Cases]
mynil [in Structures]
mynil [in Structures]
mynil' [in Structures]
MyNot.not [in Cases]
N
nandb [in Intro]NatPlayground.pred [in Types]
NatPlayground2.minus [in Recursion]
NatPlayground2.mult [in Recursion]
NatPlayground2.plus [in Recursion]
NatPlayground2.pow [in Recursion]
natset [in Sets]
natset_yikes [in Sets]
nat_to_bin [in Induction]
nat_in_tree [in Indprop]
negb [in Intro]
negb' [in Intro]
next_weekday [in Intro]
non_set_list [in Sets]
non_bst2 [in Trees]
non_bst1 [in Trees]
normalize [in Recursion]
normalize [in Induction]
nth [in Sorting2]
nth_default [in Sorting2]
nth_in_list [in Sorting2]
nth_error [in Structures]
num_leaves [in Trees]
O
oddb [in Types]option_lift [in Higherorder]
option_or [in Higherorder]
option_map' [in Structures]
option_map [in Structures]
orb [in Intro]
P
PairProjection.fst [in Structures]PairProjection.manual_grade_for_pair_exercises [in Structures]
PairProjection.pair_both [in Structures]
PairProjection.pair_swap [in Structures]
PairProjection.silly_pair [in Structures]
PairProjection.snd [in Structures]
partition [in Higherorder]
permutations [in Sorting2]
permutation_eg [in Sorting2]
permutation_false_tests [in Sorting]
permutation_true_tests [in Sorting]
plus_fact [in Propositions]
plus' [in Recursion]
plus3 [in Types]
preserves_sortedness [in Sorting2]
prod_uncurry [in Structures]
prod_curry [in Structures]
prog_eg [in Expressions]
R
remove [in Trees]remove_min [in Trees]
remove_all [in Sorting]
repeat [in Structures]
repeat' [in Structures]
repeat'' [in Structures]
repeat''' [in Structures]
rev [in Structures]
root [in Trees]
R.fR [in Indprop]
R.manual_grade_for_R_fact [in Indprop]
S
same_post_in [in Trees]same_pre_in [in Trees]
select [in Structures]
setlike_eg2 [in Indprop2]
setlike_eg1 [in Indprop2]
set_insert [in Sets]
sillyfun [in Cases]
sillyfun1 [in Cases]
size [in Induction]
size [in Trees]
sort [in Sorting2]
sort [in Sorting]
SortedSets.empty_natset [in Sets]
SortedSets.is_setlike [in Sets]
SortedSets.member [in Sets]
SortedSets.subset [in Sets]
SortedSets.union [in Sets]
SortedSets.union [in Sets]
sorted_one_through_four [in Sorting2]
sorted' [in Sorting2]
split [in Lists]
square [in Cases]
state [in Expressions]
strand [in Lists]
subset [in Indprop2]
subset [in Sets]
sum [in Structures]
sum [in Indprop]
s_compile [in Expressions]
s_execute' [in Expressions]
s_execute [in Expressions]
s_insn [in Expressions]
T
third [in Recursion]trans_eq_exercise [in Propositions]
trans_eq_example'' [in Propositions]
trans_eq_example' [in Propositions]
trans_eq_example [in Propositions]
twice [in Types]
U
union [in Sets]unique [in Sorting]
unique_sort [in Sorting]
unwrap_or [in Structures]
u_eleven [in Recursion]
u_nine [in Recursion]
u_three [in Recursion]
u_two [in Recursion]
u_one [in Recursion]
u_zero [in Recursion]
W
W [in Expressions]X
X [in Expressions]xor_option [in Structures]
Y
Y [in Expressions]Z
Z [in Expressions]zero_to_n [in Structures]
| 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 | (2019 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 | (15 entries) |
| Binder 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 | (1214 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 | (16 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 | (20 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 | (249 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 | (131 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 | (39 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 | (335 entries) |
This page has been generated by coqdoc