Volume 1: Logical Foundations

• Table of Contents
• Index
• Roadmap

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

:

_

(1238 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

:

_

(68 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

_

(25 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

_

(19 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

_

(359 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

_

(211 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

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

_

(76 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

_

(479 entries)

---

Global Index

A

A [constructor, in LF.Basics]
add1 [definition, in LF.ProofObjects]
aeval [definition, in LF.Imp]
aevalR_division [module, in LF.Imp]
aevalR_division.ADiv [constructor, in LF.Imp]
aevalR_division.aevalR [inductive, in LF.Imp]
aevalR_division.aexp [inductive, in LF.Imp]
aevalR_division.AMinus [constructor, in LF.Imp]
aevalR_division.AMult [constructor, in LF.Imp]
aevalR_division.ANum [constructor, in LF.Imp]
aevalR_division.APlus [constructor, in LF.Imp]
aevalR_division.E_ADiv [constructor, in LF.Imp]
aevalR_division.E_AMinus [constructor, in LF.Imp]
aevalR_division.E_AMult [constructor, in LF.Imp]
aevalR_division.E_ANum [constructor, in LF.Imp]
aevalR_division.E_APlus [constructor, in LF.Imp]
aevalR_division.:type_scope:x_'\\'_x [notation, in LF.Imp]
aevalR_extended [module, in LF.Imp]
aevalR_extended.AAny [constructor, in LF.Imp]
aevalR_extended.aevalR [inductive, in LF.Imp]
aevalR_extended.aexp [inductive, in LF.Imp]
aevalR_extended.AMinus [constructor, in LF.Imp]
aevalR_extended.AMult [constructor, in LF.Imp]
aevalR_extended.ANum [constructor, in LF.Imp]
aevalR_extended.APlus [constructor, in LF.Imp]
aevalR_extended.E_AMinus [constructor, in LF.Imp]
aevalR_extended.E_AMult [constructor, in LF.Imp]
aevalR_extended.E_ANum [constructor, in LF.Imp]
aevalR_extended.E_Any [constructor, in LF.Imp]
aevalR_extended.E_APlus [constructor, in LF.Imp]
aevalR_extended.:type_scope:x_'\\'_x [notation, in LF.Imp]
AExp [module, in LF.Imp]
aexp [inductive, in LF.Imp]
AExp.aeval [definition, in LF.Imp]
AExp.aevalR [inductive, in LF.Imp]
AExp.aevalR_first_try [module, in LF.Imp]
AExp.aevalR_first_try.aevalR [inductive, in LF.Imp]
AExp.aevalR_first_try.E_AMinus [constructor, in LF.Imp]
AExp.aevalR_first_try.E_AMult [constructor, in LF.Imp]
AExp.aevalR_first_try.E_ANum [constructor, in LF.Imp]
AExp.aevalR_first_try.E_APlus [constructor, in LF.Imp]
AExp.aevalR_first_try.TooHardToRead [module, in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.aevalR [inductive, in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_AMinus [constructor, in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_AMult [constructor, in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_ANum [constructor, in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_APlus [constructor, in LF.Imp]
AExp.aevalR_first_try.:type_scope:x_'\\'_x [notation, in LF.Imp]
AExp.aeval_iff_aevalR [lemma, in LF.Imp]
AExp.aeval_iff_aevalR' [lemma, in LF.Imp]
AExp.aexp [inductive, in LF.Imp]
AExp.AMinus [constructor, in LF.Imp]
AExp.AMult [constructor, in LF.Imp]
AExp.ANum [constructor, in LF.Imp]
AExp.APlus [constructor, in LF.Imp]
AExp.BAnd [constructor, in LF.Imp]
AExp.BEq [constructor, in LF.Imp]
AExp.beval [definition, in LF.Imp]
AExp.bevalR [inductive, in LF.Imp]
AExp.beval_iff_bevalR [lemma, in LF.Imp]
AExp.bexp [inductive, in LF.Imp]
AExp.BFalse [constructor, in LF.Imp]
AExp.BLe [constructor, in LF.Imp]
AExp.BNot [constructor, in LF.Imp]
AExp.BTrue [constructor, in LF.Imp]
AExp.E_AMinus [constructor, in LF.Imp]
AExp.E_AMult [constructor, in LF.Imp]
AExp.E_ANum [constructor, in LF.Imp]
AExp.E_APlus [constructor, in LF.Imp]
AExp.foo [lemma, in LF.Imp]
AExp.foo' [lemma, in LF.Imp]
AExp.In10 [lemma, in LF.Imp]
AExp.In10' [lemma, in LF.Imp]
AExp.manual_grade_for_beval_rules [definition, in LF.Imp]
AExp.optimize_0plus [definition, in LF.Imp]
AExp.optimize_0plus_b [definition, in LF.Imp]
AExp.optimize_0plus_b_sound [lemma, in LF.Imp]
AExp.optimize_0plus_sound [lemma, in LF.Imp]
AExp.optimize_0plus_sound' [lemma, in LF.Imp]
AExp.optimize_0plus_sound'' [lemma, in LF.Imp]
AExp.silly1 [lemma, in LF.Imp]
AExp.silly2 [lemma, in LF.Imp]
AExp.silly_presburger_example [definition, in LF.Imp]
AExp.test_aeval1 [definition, in LF.Imp]
AExp.test_optimize_0plus [definition, in LF.Imp]
AExp.:type_scope:x_'\\'_x [notation, in LF.Imp]
aexp1 [definition, in LF.Imp]
AId [constructor, in LF.Imp]
All [definition, in LF.Logic]
all3_spec [lemma, in LF.Induction]
All_In [lemma, in LF.Logic]
all_zero [definition, in LF.Basics]
alpha [constructor, in LF.ImpParser]
AMinus [constructor, in LF.Imp]
AMult [constructor, in LF.Imp]
andb [definition, in LF.Basics]
andb3 [definition, in LF.Basics]
andb3_exchange [lemma, in LF.Basics]
andb_commutative [lemma, in LF.Basics]
andb_commutative' [lemma, in LF.Basics]
andb_commutative'' [lemma, in LF.Basics]
andb_eq_orb [lemma, in LF.Basics]
andb_false_r [lemma, in LF.Induction]
andb_true_elim2 [lemma, in LF.Basics]
andb_true_iff [lemma, in LF.Logic]
and_assoc [lemma, in LF.Logic]
and_commut [lemma, in LF.Logic]
and_example [definition, in LF.Logic]
and_example' [definition, in LF.Logic]
and_example2 [lemma, in LF.Logic]
and_example2' [lemma, in LF.Logic]
and_example2'' [lemma, in LF.Logic]
and_example3 [lemma, in LF.Logic]
and_exercise [definition, in LF.Logic]
and_intro [lemma, in LF.Logic]
antisymmetric [definition, in LF.Rel]
ANum [constructor, in LF.Imp]
APlus [constructor, in LF.Imp]
app [definition, in LF.Poly]
App [constructor, in LF.IndProp]
apply_empty [lemma, in LF.Maps]
apply_iff_example [lemma, in LF.Logic]
app_assoc [lemma, in LF.Poly]
app_exists [lemma, in LF.IndProp]
app_length [lemma, in LF.Poly]
app_ne [lemma, in LF.IndProp]
app_nil_r [lemma, in LF.Poly]
Auto [library]
auto_example_1 [definition, in LF.Auto]
auto_example_1' [definition, in LF.Auto]
auto_example_2 [definition, in LF.Auto]
auto_example_3 [definition, in LF.Auto]
auto_example_4 [definition, in LF.Auto]
auto_example_6 [definition, in LF.Auto]
auto_example_6' [definition, in LF.Auto]
auto_example_7 [definition, in LF.Auto]
auto_example_7' [definition, in LF.Auto]

B

B [constructor, in LF.Basics]
BAnd [constructor, in LF.Imp]
bar [definition, in LF.Tactics]
Basics [library]
baz [inductive, in LF.Lists]
Baz1 [constructor, in LF.Lists]
Baz2 [constructor, in LF.Lists]
bempty [constructor, in LF.IndPrinciples]
BEq [constructor, in LF.Imp]
beval [definition, in LF.Imp]
bexp [inductive, in LF.Imp]
bexp1 [definition, in LF.Imp]
BFalse [constructor, in LF.Imp]
Bib [library]
bignumber [definition, in LF.ImpParser]
bin [inductive, in LF.Basics]
bin_to_nat [definition, in LF.Basics]
bit [inductive, in LF.Basics]
bits [constructor, in LF.Basics]
black [constructor, in LF.Basics]
BLe [constructor, in LF.Imp]
bleaf [constructor, in LF.IndPrinciples]
blue [constructor, in LF.Basics]
blue [constructor, in LF.IndPrinciples]
BNot [constructor, in LF.Imp]
bool [inductive, in LF.Basics]
boollist [inductive, in LF.Poly]
bool_cons [constructor, in LF.Poly]
bool_fn_applied_thrice [lemma, in LF.Tactics]
bool_nil [constructor, in LF.Poly]
bool_to_bexp [definition, in LF.Imp]
BreakImp [module, in LF.Imp]
BreakImp.break_ignore [lemma, in LF.Imp]
BreakImp.CAss [constructor, in LF.Imp]
BreakImp.CBreak [constructor, in LF.Imp]
BreakImp.ceval [inductive, in LF.Imp]
BreakImp.ceval_deterministic [lemma, in LF.Imp]
BreakImp.CIf [constructor, in LF.Imp]
BreakImp.com [inductive, in LF.Imp]
BreakImp.CSeq [constructor, in LF.Imp]
BreakImp.CSkip [constructor, in LF.Imp]
BreakImp.CWhile [constructor, in LF.Imp]
BreakImp.E_Skip [constructor, in LF.Imp]
BreakImp.result [inductive, in LF.Imp]
BreakImp.SBreak [constructor, in LF.Imp]
BreakImp.SContinue [constructor, in LF.Imp]
BreakImp.while_break_true [lemma, in LF.Imp]
BreakImp.while_continue [lemma, in LF.Imp]
BreakImp.while_stops_on_break [lemma, in LF.Imp]
BreakImp.::x_'::='_x [notation, in LF.Imp]
BreakImp.::x_';;'_x [notation, in LF.Imp]
BreakImp.::x_'=['_x_']=>'_x_'/'_x [notation, in LF.Imp]
BreakImp.::'BREAK' [notation, in LF.Imp]
BreakImp.::'SKIP' [notation, in LF.Imp]
BreakImp.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in LF.Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [notation, in LF.Imp]
BTrue [constructor, in LF.Imp]
byntree [inductive, in LF.IndPrinciples]
B₀ [constructor, in LF.Basics]
B₁ [constructor, in LF.Basics]

C

c [definition, in LF.IndProp]
CAss [constructor, in LF.Imp]
ceval [inductive, in LF.Imp]
ceval'_example1 [definition, in LF.Auto]
ceval_and_ceval_step_coincide [lemma, in LF.ImpCEvalFun]
ceval_deterministic [lemma, in LF.Auto]
ceval_deterministic [lemma, in LF.Imp]
ceval_deterministic' [lemma, in LF.ImpCEvalFun]
ceval_deterministic' [lemma, in LF.Auto]
ceval_deterministic'' [lemma, in LF.Auto]
ceval_deterministic''' [lemma, in LF.Auto]
ceval_deterministic'''' [lemma, in LF.Auto]
ceval_deterministic''''' [lemma, in LF.Auto]
ceval_deterministic'_alt [lemma, in LF.Auto]
ceval_example1 [definition, in LF.Auto]
ceval_example1 [definition, in LF.Imp]
ceval_example2 [definition, in LF.Imp]
ceval_fun_no_while [definition, in LF.Imp]
ceval_step [definition, in LF.ImpCEvalFun]
ceval_step1 [definition, in LF.ImpCEvalFun]
ceval_step2 [definition, in LF.ImpCEvalFun]
ceval_step3 [definition, in LF.ImpCEvalFun]
ceval_step_more [lemma, in LF.ImpCEvalFun]
ceval_step__ceval [lemma, in LF.ImpCEvalFun]
ceval__ceval_step [lemma, in LF.ImpCEvalFun]
Char [constructor, in LF.IndProp]
chartype [inductive, in LF.ImpParser]
char_eps_suffix [lemma, in LF.IndProp]
char_nomatch_char [lemma, in LF.IndProp]
CIf [constructor, in LF.Imp]
classifyChar [definition, in LF.ImpParser]
clos_refl_trans [inductive, in LF.Rel]
clos_refl_trans_1n [inductive, in LF.Rel]
color [inductive, in LF.Basics]
com [inductive, in LF.Imp]
combine [definition, in LF.Poly]
combine_odd_even [definition, in LF.Logic]
combine_odd_even_elim_even [lemma, in LF.Logic]
combine_odd_even_elim_odd [lemma, in LF.Logic]
combine_odd_even_intro [lemma, in LF.Logic]
combine_split [lemma, in LF.Tactics]
cons [constructor, in LF.Poly]
constfun [definition, in LF.Poly]
constfun_example1 [definition, in LF.Poly]
constfun_example2 [definition, in LF.Poly]
cons' [constructor, in LF.Poly]
contradiction_implies_anything [lemma, in LF.Logic]
contrapositive [lemma, in LF.Logic]
count [definition, in LF.IndProp]
countoddmembers' [definition, in LF.Poly]
CSeq [constructor, in LF.Imp]
CSkip [constructor, in LF.Imp]
CWhile [constructor, in LF.Imp]
C₁ [constructor, in LF.IndPrinciples]
C₂ [constructor, in LF.IndPrinciples]

D

d [definition, in LF.IndProp]
day [inductive, in LF.Basics]
derive [definition, in LF.IndProp]
derives [definition, in LF.IndProp]
derive_corr [lemma, in LF.IndProp]
de_morgan_not_and_not [definition, in LF.Logic]
digit [constructor, in LF.ImpParser]
discriminate_ex₁ [lemma, in LF.Tactics]
discriminate_ex₂ [lemma, in LF.Tactics]
discriminate_ex₃ [definition, in LF.Tactics]
dist_exists_or [lemma, in LF.Logic]
dist_not_exists [lemma, in LF.Logic]
doit3times [definition, in LF.Poly]
double [definition, in LF.Induction]
double_injective [lemma, in LF.Tactics]
double_injective_FAILED [lemma, in LF.Tactics]
double_injective_take2 [lemma, in LF.Tactics]
double_injective_take2_FAILED [lemma, in LF.Tactics]
double_neg [lemma, in LF.Logic]
double_negation_elimination [definition, in LF.Logic]
double_plus [lemma, in LF.Induction]

E

eauto_example [definition, in LF.Auto]
eg₁ [definition, in LF.ImpParser]
eg₂ [definition, in LF.ImpParser]
empty [definition, in LF.Maps]
EmptySet [constructor, in LF.IndProp]
EmptyStr [constructor, in LF.IndProp]
empty_is_empty [lemma, in LF.IndProp]
empty_matches_eps [lemma, in LF.IndProp]
empty_nomatch_ne [lemma, in LF.IndProp]
empty_st [definition, in LF.Imp]
eqb [definition, in LF.Basics]
eqbP [lemma, in LF.IndProp]
eqbP_practice [lemma, in LF.IndProp]
eqb_eq [lemma, in LF.Logic]
eqb_id [definition, in LF.Lists]
eqb_id_refl [lemma, in LF.Lists]
eqb_id_true [lemma, in LF.Tactics]
eqb_list [definition, in LF.Logic]
eqb_list_true_iff [lemma, in LF.Logic]
eqb_neq [lemma, in LF.Logic]
eqb_refl [lemma, in LF.Induction]
eqb_string [definition, in LF.Maps]
eqb_stringP [lemma, in LF.Maps]
eqb_string_false_iff [lemma, in LF.Maps]
eqb_string_refl [lemma, in LF.Maps]
eqb_string_true_iff [lemma, in LF.Maps]
eqb_sym [lemma, in LF.Tactics]
eqb_trans [lemma, in LF.Tactics]
eqb_true [lemma, in LF.Tactics]
eqb_0_l [lemma, in LF.Tactics]
equivalence [definition, in LF.Rel]
even [inductive, in LF.IndProp]
evenb [definition, in LF.Basics]
evenb_double [lemma, in LF.Logic]
evenb_double_conv [lemma, in LF.Logic]
evenb_S [lemma, in LF.Induction]
even' [inductive, in LF.IndProp]
even'_ev [lemma, in LF.IndProp]
even'_sum [constructor, in LF.IndProp]
even'_0 [constructor, in LF.IndProp]
even'_2 [constructor, in LF.IndProp]
even5_nonsense [lemma, in LF.IndProp]
even_bool_prop [lemma, in LF.Logic]
even_1000 [definition, in LF.Logic]
even_1000' [definition, in LF.Logic]
even_1000'' [definition, in LF.Logic]
even_42_bool [definition, in LF.Logic]
even_42_prop [definition, in LF.Logic]
evSS_ev [lemma, in LF.IndProp]
evSS_ev [lemma, in LF.IndProp]
evSS_ev' [lemma, in LF.IndProp]
ev_double [lemma, in LF.IndProp]
ev_even [lemma, in LF.IndProp]
ev_even_firsttry [lemma, in LF.IndProp]
ev_even_iff [lemma, in LF.IndProp]
ev_ev' [lemma, in LF.IndPrinciples]
ev_ev__ev [lemma, in LF.IndProp]
ev_inversion [lemma, in LF.IndProp]
ev_minus2 [lemma, in LF.IndProp]
ev_plus2 [definition, in LF.ProofObjects]
ev_plus2' [definition, in LF.ProofObjects]
ev_plus2'' [definition, in LF.ProofObjects]
ev_plus4 [lemma, in LF.ProofObjects]
ev_plus4 [lemma, in LF.IndProp]
ev_plus4' [definition, in LF.ProofObjects]
ev_plus4'' [definition, in LF.ProofObjects]
ev_plus_plus [lemma, in LF.IndProp]
ev_SS [constructor, in LF.IndProp]
ev_sum [lemma, in LF.IndProp]
ev_0 [constructor, in LF.IndProp]
ev_4 [lemma, in LF.ProofObjects]
ev_4 [lemma, in LF.IndProp]
ev_4' [lemma, in LF.IndProp]
ev_4' [lemma, in LF.ProofObjects]
ev_4'' [lemma, in LF.ProofObjects]
ev_4''' [definition, in LF.ProofObjects]
ev_8 [lemma, in LF.ProofObjects]
ev_8' [definition, in LF.ProofObjects]
examplemap [definition, in LF.Maps]
examplemap' [definition, in LF.Maps]
examplepmap [definition, in LF.Maps]
example_aexp [definition, in LF.Imp]
example_bexp [definition, in LF.Imp]
example_empty [definition, in LF.Maps]
excluded_middle [definition, in LF.Logic]
excluded_middle_irrefutable [lemma, in LF.Logic]
Exercises [module, in LF.Poly]
Exercises.Church [module, in LF.Poly]
Exercises.Church.cnat [definition, in LF.Poly]
Exercises.Church.exp [definition, in LF.Poly]
Exercises.Church.exp_1 [definition, in LF.Poly]
Exercises.Church.exp_2 [definition, in LF.Poly]
Exercises.Church.exp_3 [definition, in LF.Poly]
Exercises.Church.mult [definition, in LF.Poly]
Exercises.Church.mult_1 [definition, in LF.Poly]
Exercises.Church.mult_2 [definition, in LF.Poly]
Exercises.Church.mult_3 [definition, in LF.Poly]
Exercises.Church.one [definition, in LF.Poly]
Exercises.Church.plus [definition, in LF.Poly]
Exercises.Church.plus_1 [definition, in LF.Poly]
Exercises.Church.plus_2 [definition, in LF.Poly]
Exercises.Church.plus_3 [definition, in LF.Poly]
Exercises.Church.succ [definition, in LF.Poly]
Exercises.Church.succ_1 [definition, in LF.Poly]
Exercises.Church.succ_2 [definition, in LF.Poly]
Exercises.Church.succ_3 [definition, in LF.Poly]
Exercises.Church.three [definition, in LF.Poly]
Exercises.Church.two [definition, in LF.Poly]
Exercises.Church.zero [definition, in LF.Poly]
Exercises.curry_uncurry [lemma, in LF.Poly]
Exercises.fold_length [definition, in LF.Poly]
Exercises.fold_length_correct [lemma, in LF.Poly]
Exercises.fold_map [definition, in LF.Poly]
Exercises.manual_grade_for_fold_map [definition, in LF.Poly]
Exercises.manual_grade_for_informal_proof [definition, in LF.Poly]
Exercises.prod_curry [definition, in LF.Poly]
Exercises.prod_uncurry [definition, in LF.Poly]
Exercises.test_fold_length1 [definition, in LF.Poly]
Exercises.test_map1' [definition, in LF.Poly]
Exercises.uncurry_curry [lemma, in LF.Poly]
existsb [definition, in LF.Tactics]
existsb' [definition, in LF.Tactics]
existsb_existsb' [lemma, in LF.Tactics]
exists_example_2 [lemma, in LF.Logic]
exp [definition, in LF.Basics]
expect [definition, in LF.ImpParser]
exp_match [inductive, in LF.IndProp]
ExSet [inductive, in LF.IndPrinciples]
Extraction [library]
ex_falso_quodlibet [lemma, in LF.Logic]
E_Ass [constructor, in LF.Imp]
E_IfFalse [constructor, in LF.Imp]
E_IfTrue [constructor, in LF.Imp]
E_Seq [constructor, in LF.Imp]
E_Skip [constructor, in LF.Imp]
E_WhileFalse [constructor, in LF.Imp]
E_WhileTrue [constructor, in LF.Imp]

F

factorial [definition, in LF.Basics]
fact_in_coq [definition, in LF.Imp]
false [constructor, in LF.Basics]
false_eqb_string [lemma, in LF.Maps]
filter [definition, in LF.Poly]
filter_even_gt₇ [definition, in LF.Poly]
filter_exercise [lemma, in LF.Tactics]
filter_not_empty_In [lemma, in LF.IndProp]
filter_not_empty_In' [lemma, in LF.IndProp]
firstExpect [definition, in LF.ImpParser]
flat_map [definition, in LF.Poly]
fold [definition, in LF.Poly]
fold_example1 [definition, in LF.Poly]
fold_example2 [definition, in LF.Poly]
fold_example3 [definition, in LF.Poly]
foo [definition, in LF.Tactics]
foo' [inductive, in LF.IndPrinciples]
forallb [definition, in LF.Tactics]
forallb [definition, in LF.Logic]
forallb_true_iff [lemma, in LF.Logic]
four_is_even [lemma, in LF.Logic]
friday [constructor, in LF.Basics]
fst [definition, in LF.Poly]
ftrue [definition, in LF.Poly]
functional_extensionality [axiom, in LF.Logic]
function_equality_ex₁ [definition, in LF.Logic]
function_equality_ex₂ [definition, in LF.Logic]
function_equality_ex₂ [definition, in LF.Logic]
f_equal [lemma, in LF.Tactics]

G

green [constructor, in LF.Basics]
green [constructor, in LF.IndPrinciples]

H

hd_error [definition, in LF.Poly]

I

Id [constructor, in LF.Lists]
id [inductive, in LF.Lists]
identity_fn_applied_twice [lemma, in LF.Basics]
iff_refl [lemma, in LF.Logic]
iff_reflect [lemma, in LF.IndProp]
iff_sym [lemma, in LF.Logic]
iff_trans [lemma, in LF.Logic]
Imp [library]
ImpCEvalFun [library]
implies_to_or [definition, in LF.Logic]
ImpParser [library]
In [definition, in LF.Logic]
incr [definition, in LF.Basics]
IndPrinciples [library]
IndProp [library]
Induction [library]
injection_ex₁ [lemma, in LF.Tactics]
injection_ex₂ [lemma, in LF.Tactics]
injection_ex₃ [definition, in LF.Tactics]
injective [definition, in LF.Logic]
inversion_ex₁ [lemma, in LF.IndProp]
inversion_ex₂ [lemma, in LF.IndProp]
In_app_iff [lemma, in LF.Logic]
In_example_1 [definition, in LF.Logic]
In_example_2 [definition, in LF.Logic]
In_map [lemma, in LF.Logic]
In_map_iff [lemma, in LF.Logic]
in_not_nil [lemma, in LF.Logic]
in_not_nil_42 [lemma, in LF.Logic]
in_not_nil_42_take2 [lemma, in LF.Logic]
in_not_nil_42_take3 [lemma, in LF.Logic]
in_not_nil_42_take4 [lemma, in LF.Logic]
in_not_nil_42_take5 [lemma, in LF.Logic]
in_re_match [lemma, in LF.IndProp]
in_split [lemma, in LF.IndProp]
isAlpha [definition, in LF.ImpParser]
isDigit [definition, in LF.ImpParser]
isLowerAlpha [definition, in LF.ImpParser]
isred [definition, in LF.Basics]
isWhite [definition, in LF.ImpParser]
is_der [definition, in LF.IndProp]
is_even_prime [definition, in LF.Logic]
is_fortytwo [definition, in LF.Auto]
is_three [definition, in LF.Logic]

L

le [inductive, in LF.IndPrinciples]
leaf [constructor, in LF.IndPrinciples]
leb [definition, in LF.Basics]
leb_complete [lemma, in LF.IndProp]
leb_correct [lemma, in LF.IndProp]
leb_iff [lemma, in LF.IndProp]
leb_refl [lemma, in LF.Induction]
leb_true_trans [lemma, in LF.IndProp]
lemma_application_ex [definition, in LF.Logic]
length [definition, in LF.Poly]
length_is_1 [definition, in LF.Poly]
le_antisym [lemma, in LF.Auto]
le_antisymmetric [lemma, in LF.Rel]
le_n [constructor, in LF.IndPrinciples]
le_not_a_partial_function [lemma, in LF.Rel]
le_not_symmetric [lemma, in LF.Rel]
le_order [lemma, in LF.Rel]
le_plus_l [lemma, in LF.IndProp]
le_reflexive [lemma, in LF.Rel]
le_S [constructor, in LF.IndPrinciples]
le_Sn_le [lemma, in LF.Rel]
le_Sn_n [lemma, in LF.Rel]
le_step [lemma, in LF.Rel]
le_S_n [lemma, in LF.Rel]
le_trans [lemma, in LF.IndProp]
le_trans [lemma, in LF.Rel]
list [inductive, in LF.Poly]
Lists [library]
list' [inductive, in LF.Poly]
list123 [definition, in LF.Poly]
list123' [definition, in LF.Poly]
list123'' [definition, in LF.Poly]
list123''' [definition, in LF.Poly]
list_of_string [definition, in LF.ImpParser]
Logic [library]
loop [definition, in LF.Imp]
loop_never_stops [lemma, in LF.Imp]
lt [definition, in LF.IndProp]
ltb [definition, in LF.Basics]
lt_S [lemma, in LF.IndProp]
lt_trans [lemma, in LF.Rel]
lt_trans' [lemma, in LF.Rel]
lt_trans'' [lemma, in LF.Rel]

M

manual_grade_for_baz_num_elts [definition, in LF.Lists]
manual_grade_for_binary [definition, in LF.Basics]
manual_grade_for_binary_commute [definition, in LF.Induction]
manual_grade_for_binary_inverse_a [definition, in LF.Induction]
manual_grade_for_binary_inverse_b [definition, in LF.Induction]
manual_grade_for_binary_inverse_c [definition, in LF.Induction]
manual_grade_for_ceval_step__ceval_inf [definition, in LF.ImpCEvalFun]
manual_grade_for_check_repeats [definition, in LF.IndProp]
manual_grade_for_destruct_induction [definition, in LF.Induction]
manual_grade_for_double_neg_inf [definition, in LF.Logic]
manual_grade_for_filter_challenge [definition, in LF.IndProp]
manual_grade_for_fold_types_different [definition, in LF.Poly]
manual_grade_for_informal_not_PNP [definition, in LF.Logic]
manual_grade_for_informal_proof [definition, in LF.Tactics]
manual_grade_for_mumble_grumble [definition, in LF.Poly]
manual_grade_for_negation_fn_applied_twice [definition, in LF.Basics]
manual_grade_for_NoDup_disjoint_etc [definition, in LF.IndProp]
manual_grade_for_nostutter [definition, in LF.IndProp]
manual_grade_for_no_whiles_terminating [definition, in LF.Imp]
manual_grade_for_pal_pal_app_rev_pal_rev [definition, in LF.IndProp]
manual_grade_for_plus_comm_informal [definition, in LF.Induction]
manual_grade_for_split_combine [definition, in LF.Tactics]
manual_grade_for_XtimesYinZ_spec [definition, in LF.Imp]
many [definition, in LF.ImpParser]
many_helper [definition, in LF.ImpParser]
map [definition, in LF.Poly]
MApp [constructor, in LF.IndProp]
Maps [library]
map_rev [lemma, in LF.Poly]
matches_regex [definition, in LF.IndProp]
match_eps [definition, in LF.IndProp]
match_eps_refl [lemma, in LF.IndProp]
MChar [constructor, in LF.IndProp]
MEmpty [constructor, in LF.IndProp]
minustwo [definition, in LF.Basics]
minus_diag [lemma, in LF.Induction]
monday [constructor, in LF.Basics]
monochrome [definition, in LF.Basics]
MStarApp [constructor, in LF.IndProp]
MStar' [lemma, in LF.IndProp]
MStar'' [lemma, in LF.IndProp]
MStar0 [constructor, in LF.IndProp]
MStar1 [lemma, in LF.IndProp]
mult_assoc [lemma, in LF.Induction]
mult_comm [lemma, in LF.Induction]
mult_eq_0 [lemma, in LF.Logic]
mult_plus_distr_r [lemma, in LF.Induction]
mult_S_1 [lemma, in LF.Basics]
mult_0 [lemma, in LF.Logic]
mult_0_l [lemma, in LF.Basics]
mult_0_plus [lemma, in LF.Basics]
mult_0_plus' [lemma, in LF.Induction]
mult_0_r [lemma, in LF.Induction]
mult_0_r' [lemma, in LF.IndPrinciples]
mult_0_r'' [lemma, in LF.IndPrinciples]
mult_0_3 [lemma, in LF.Logic]
mult_1_l [lemma, in LF.Induction]
MumbleGrumble [module, in LF.Poly]
MumbleGrumble.a [constructor, in LF.Poly]
MumbleGrumble.b [constructor, in LF.Poly]
MumbleGrumble.c [constructor, in LF.Poly]
MumbleGrumble.d [constructor, in LF.Poly]
MumbleGrumble.e [constructor, in LF.Poly]
MumbleGrumble.grumble [inductive, in LF.Poly]
MumbleGrumble.mumble [inductive, in LF.Poly]
MUnionL [constructor, in LF.IndProp]
MUnionR [constructor, in LF.IndProp]
MUnion' [lemma, in LF.IndProp]
MyEquality [module, in LF.ProofObjects]
MyEquality.eq [inductive, in LF.ProofObjects]
MyEquality.equality__leibniz_equality [lemma, in LF.ProofObjects]
MyEquality.eq_refl [constructor, in LF.ProofObjects]
MyEquality.four [lemma, in LF.ProofObjects]
MyEquality.four' [definition, in LF.ProofObjects]
MyEquality.leibniz_equality__equality [lemma, in LF.ProofObjects]
MyEquality.singleton [definition, in LF.ProofObjects]
MyEquality.:type_scope:x_'=='_x [notation, in LF.ProofObjects]
MyIff [module, in LF.Logic]
MyIff.iff [definition, in LF.Logic]
->'_x">MyIff.:type_scope:x_'<->'_x [notation, in LF.Logic]
mynil [definition, in LF.Poly]
mynil [definition, in LF.Poly]
mynil' [definition, in LF.Poly]
MyNot [module, in LF.Logic]
MyNot.not [definition, in LF.Logic]
MyNot.:type_scope:'~'_x [notation, in LF.Logic]

N

nandb [definition, in LF.Basics]
natlist [inductive, in LF.IndPrinciples]
NatList [module, in LF.Lists]
NatList.add [definition, in LF.Lists]
NatList.alternate [definition, in LF.Lists]
NatList.app [definition, in LF.Lists]
NatList.app_assoc [lemma, in LF.Lists]
NatList.app_assoc4 [lemma, in LF.Lists]
NatList.app_length [lemma, in LF.Lists]
NatList.app_nil_r [lemma, in LF.Lists]
NatList.bag [definition, in LF.Lists]
NatList.cons [constructor, in LF.Lists]
NatList.count [definition, in LF.Lists]
NatList.countoddmembers [definition, in LF.Lists]
NatList.count_member_nonzero [lemma, in LF.Lists]
NatList.eqblist [definition, in LF.Lists]
NatList.eqblist_refl [lemma, in LF.Lists]
NatList.fst [definition, in LF.Lists]
NatList.fst' [definition, in LF.Lists]
NatList.fst_swap_is_snd [lemma, in LF.Lists]
NatList.hd [definition, in LF.Lists]
NatList.hd_error [definition, in LF.Lists]
NatList.leb_n_Sn [lemma, in LF.Lists]
NatList.length [definition, in LF.Lists]
NatList.manual_grade_for_bag_theorem [definition, in LF.Lists]
NatList.manual_grade_for_rev_injective [definition, in LF.Lists]
NatList.member [definition, in LF.Lists]
NatList.mylist [definition, in LF.Lists]
NatList.mylist1 [definition, in LF.Lists]
NatList.mylist2 [definition, in LF.Lists]
NatList.mylist3 [definition, in LF.Lists]
NatList.natlist [inductive, in LF.Lists]
NatList.natoption [inductive, in LF.Lists]
NatList.natprod [inductive, in LF.Lists]
NatList.nil [constructor, in LF.Lists]
NatList.nil_app [lemma, in LF.Lists]
NatList.None [constructor, in LF.Lists]
NatList.nonzeros [definition, in LF.Lists]
NatList.nonzeros_app [lemma, in LF.Lists]
NatList.nth_bad [definition, in LF.Lists]
NatList.nth_error [definition, in LF.Lists]
NatList.nth_error' [definition, in LF.Lists]
NatList.oddmembers [definition, in LF.Lists]
NatList.option_elim [definition, in LF.Lists]
NatList.option_elim_hd [lemma, in LF.Lists]
NatList.pair [constructor, in LF.Lists]
NatList.remove_all [definition, in LF.Lists]
NatList.remove_does_not_increase_count [lemma, in LF.Lists]
NatList.remove_one [definition, in LF.Lists]
NatList.repeat [definition, in LF.Lists]
NatList.rev [definition, in LF.Lists]
NatList.rev_app_distr [lemma, in LF.Lists]
NatList.rev_involutive [lemma, in LF.Lists]
NatList.rev_length [lemma, in LF.Lists]
NatList.rev_length_firsttry [lemma, in LF.Lists]
NatList.snd [definition, in LF.Lists]
NatList.snd' [definition, in LF.Lists]
NatList.snd_fst_is_swap [lemma, in LF.Lists]
NatList.Some [constructor, in LF.Lists]
NatList.subset [definition, in LF.Lists]
NatList.sum [definition, in LF.Lists]
NatList.surjective_pairing [lemma, in LF.Lists]
NatList.surjective_pairing' [lemma, in LF.Lists]
NatList.surjective_pairing_stuck [lemma, in LF.Lists]
NatList.swap_pair [definition, in LF.Lists]
NatList.test_add1 [definition, in LF.Lists]
NatList.test_add2 [definition, in LF.Lists]
NatList.test_alternate1 [definition, in LF.Lists]
NatList.test_alternate2 [definition, in LF.Lists]
NatList.test_alternate3 [definition, in LF.Lists]
NatList.test_alternate4 [definition, in LF.Lists]
NatList.test_app1 [definition, in LF.Lists]
NatList.test_app2 [definition, in LF.Lists]
NatList.test_app3 [definition, in LF.Lists]
NatList.test_countoddmembers1 [definition, in LF.Lists]
NatList.test_countoddmembers2 [definition, in LF.Lists]
NatList.test_countoddmembers3 [definition, in LF.Lists]
NatList.test_count1 [definition, in LF.Lists]
NatList.test_count2 [definition, in LF.Lists]
NatList.test_eqblist1 [definition, in LF.Lists]
NatList.test_eqblist2 [definition, in LF.Lists]
NatList.test_eqblist3 [definition, in LF.Lists]
NatList.test_hd₁ [definition, in LF.Lists]
NatList.test_hd₂ [definition, in LF.Lists]
NatList.test_hd_error1 [definition, in LF.Lists]
NatList.test_hd_error2 [definition, in LF.Lists]
NatList.test_hd_error3 [definition, in LF.Lists]
NatList.test_member1 [definition, in LF.Lists]
NatList.test_member2 [definition, in LF.Lists]
NatList.test_nonzeros [definition, in LF.Lists]
NatList.test_nth_error1 [definition, in LF.Lists]
NatList.test_nth_error2 [definition, in LF.Lists]
NatList.test_nth_error3 [definition, in LF.Lists]
NatList.test_oddmembers [definition, in LF.Lists]
NatList.test_remove_all1 [definition, in LF.Lists]
NatList.test_remove_all2 [definition, in LF.Lists]
NatList.test_remove_all3 [definition, in LF.Lists]
NatList.test_remove_all4 [definition, in LF.Lists]
NatList.test_remove_one1 [definition, in LF.Lists]
NatList.test_remove_one2 [definition, in LF.Lists]
NatList.test_remove_one3 [definition, in LF.Lists]
NatList.test_remove_one4 [definition, in LF.Lists]
NatList.test_rev1 [definition, in LF.Lists]
NatList.test_rev2 [definition, in LF.Lists]
NatList.test_subset1 [definition, in LF.Lists]
NatList.test_subset2 [definition, in LF.Lists]
NatList.test_sum1 [definition, in LF.Lists]
NatList.test_tl [definition, in LF.Lists]
NatList.tl [definition, in LF.Lists]
NatList.tl_length_pred [lemma, in LF.Lists]
NatList.::x_'++'_x [notation, in LF.Lists]
NatList.::x_'::'_x [notation, in LF.Lists]
NatList.::'('_x_','_x_')' [notation, in LF.Lists]
NatList.::'['_x_';'_'..'_';'_x_']' [notation, in LF.Lists]
NatList.::'['_']' [notation, in LF.Lists]
natlist1 [inductive, in LF.IndPrinciples]
NatPlayground [module, in LF.Basics]
NatPlayground.nat [inductive, in LF.Basics]
NatPlayground.nat' [inductive, in LF.Basics]
NatPlayground.O [constructor, in LF.Basics]
NatPlayground.pred [definition, in LF.Basics]
NatPlayground.S [constructor, in LF.Basics]
NatPlayground.stop [constructor, in LF.Basics]
NatPlayground.tick [constructor, in LF.Basics]
NatPlayground2 [module, in LF.Basics]
NatPlayground2.minus [definition, in LF.Basics]
NatPlayground2.mult [definition, in LF.Basics]
NatPlayground2.plus [definition, in LF.Basics]
NatPlayground2.test_mult1 [definition, in LF.Basics]
nat_bin_nat [lemma, in LF.Induction]
nat_to_bin [definition, in LF.Induction]
nbranch [constructor, in LF.IndPrinciples]
ncons [constructor, in LF.IndPrinciples]
negb [definition, in LF.Basics]
negb_involutive [lemma, in LF.Basics]
next_even [inductive, in LF.IndProp]
next_nat [inductive, in LF.IndProp]
next_nat_closure_is_le [lemma, in LF.Rel]
next_nat_partial_function [lemma, in LF.Rel]
next_weekday [definition, in LF.Basics]
ne_1 [constructor, in LF.IndProp]
ne_2 [constructor, in LF.IndProp]
nil [constructor, in LF.Poly]
nil' [constructor, in LF.Poly]
nn [constructor, in LF.IndProp]
nnil [constructor, in LF.IndPrinciples]
nnil1 [constructor, in LF.IndPrinciples]
no [constructor, in LF.IndPrinciples]
node [constructor, in LF.IndPrinciples]
NoneE [constructor, in LF.ImpParser]
nostutter [inductive, in LF.IndProp]
not_both_true_and_false [lemma, in LF.Logic]
not_equiv_false [lemma, in LF.IndProp]
not_even_1001 [definition, in LF.Logic]
not_even_1001' [definition, in LF.Logic]
not_exists_dist [lemma, in LF.Logic]
not_False [lemma, in LF.Logic]
not_implies_our_not [lemma, in LF.Logic]
not_true_iff_false [lemma, in LF.Logic]
not_true_is_false [lemma, in LF.Logic]
not_true_is_false' [lemma, in LF.Logic]
no_whiles [definition, in LF.Imp]
no_whilesR [inductive, in LF.Imp]
no_whiles_eqv [lemma, in LF.Imp]
nsnoc1 [constructor, in LF.IndPrinciples]
nth_error [definition, in LF.Poly]
nth_error_after_last [lemma, in LF.Tactics]
null_matches_none [lemma, in LF.IndProp]
nybble [inductive, in LF.Basics]
n_le_m__Sn_le_Sm [lemma, in LF.IndProp]

O

oddb [definition, in LF.Basics]
one_not_even [lemma, in LF.IndProp]
one_not_even' [lemma, in LF.IndProp]
optionE [inductive, in LF.ImpParser]
OptionPlayground [module, in LF.Poly]
OptionPlayground.None [constructor, in LF.Poly]
OptionPlayground.option [inductive, in LF.Poly]
OptionPlayground.Some [constructor, in LF.Poly]
option_map [definition, in LF.Poly]
orb [definition, in LF.Basics]
orb_true_iff [lemma, in LF.Logic]
order [definition, in LF.Rel]
or_assoc [lemma, in LF.Logic]
or_commut [lemma, in LF.Logic]
or_distributes_over_and [lemma, in LF.Logic]
or_example [lemma, in LF.Logic]
or_intro [lemma, in LF.Logic]
other [constructor, in LF.ImpParser]
O_le_n [lemma, in LF.IndProp]

P

pair [constructor, in LF.Poly]
parse [definition, in LF.ImpParser]
parseAExp [definition, in LF.ImpParser]
parseAtomicExp [definition, in LF.ImpParser]
parseBExp [definition, in LF.ImpParser]
parseConjunctionExp [definition, in LF.ImpParser]
parseIdentifier [definition, in LF.ImpParser]
parseNumber [definition, in LF.ImpParser]
parsePrimaryExp [definition, in LF.ImpParser]
parseProductExp [definition, in LF.ImpParser]
parser [definition, in LF.ImpParser]
parseSequencedCommand [definition, in LF.ImpParser]
parseSimpleCommand [definition, in LF.ImpParser]
parseSumExp [definition, in LF.ImpParser]
PartialMap [module, in LF.Lists]
PartialMap.empty [constructor, in LF.Lists]
PartialMap.find [definition, in LF.Lists]
PartialMap.partial_map [inductive, in LF.Lists]
PartialMap.record [constructor, in LF.Lists]
PartialMap.update [definition, in LF.Lists]
PartialMap.update_eq [lemma, in LF.Lists]
PartialMap.update_neq [lemma, in LF.Lists]
partial_function [definition, in LF.Rel]
partial_map [definition, in LF.Maps]
partition [definition, in LF.Poly]
peirce [definition, in LF.Logic]
pigeonhole_principle [lemma, in LF.IndProp]
Playground [module, in LF.IndProp]
Playground.le [inductive, in LF.IndProp]
Playground.le_n [constructor, in LF.IndProp]
Playground.le_S [constructor, in LF.IndProp]
Playground.test_le₁ [lemma, in LF.IndProp]
Playground.test_le₂ [lemma, in LF.IndProp]
Playground.test_le₃ [lemma, in LF.IndProp]
Playground.::x_'<='_x [notation, in LF.IndProp]
plus' [definition, in LF.Basics]
plus2 [definition, in LF.Imp]
plus2_spec [lemma, in LF.Imp]
plus3 [definition, in LF.Poly]
plus_assoc [lemma, in LF.Induction]
plus_assoc' [lemma, in LF.Induction]
plus_assoc' [lemma, in LF.IndPrinciples]
plus_assoc'' [lemma, in LF.Induction]
plus_ble_compat_l [lemma, in LF.Induction]
plus_comm [lemma, in LF.Induction]
plus_comm' [lemma, in LF.IndPrinciples]
plus_comm'' [lemma, in LF.IndPrinciples]
plus_comm3 [lemma, in LF.Logic]
plus_comm3_take2 [lemma, in LF.Logic]
plus_comm3_take3 [lemma, in LF.Logic]
plus_eqb_example [lemma, in LF.Logic]
plus_fact [definition, in LF.Logic]
plus_fact_is_true [lemma, in LF.Logic]
plus_id_example [lemma, in LF.Basics]
plus_id_exercise [lemma, in LF.Basics]
plus_lt [lemma, in LF.IndProp]
plus_n_n_injective [lemma, in LF.Tactics]
plus_n_O [lemma, in LF.Induction]
plus_n_O_firsttry [lemma, in LF.Induction]
plus_n_O_secondtry [lemma, in LF.Induction]
plus_n_Sm [lemma, in LF.Induction]
plus_one_r' [lemma, in LF.IndPrinciples]
plus_O_n [lemma, in LF.Basics]
plus_O_n' [lemma, in LF.Basics]
plus_rearrange [lemma, in LF.Induction]
plus_rearrange_firsttry [lemma, in LF.Induction]
plus_swap [lemma, in LF.Induction]
plus_swap' [lemma, in LF.Induction]
plus_1_l [lemma, in LF.Basics]
plus_1_neq_0 [lemma, in LF.Basics]
plus_1_neq_0' [lemma, in LF.Basics]
plus_1_neq_0_firsttry [lemma, in LF.Basics]
plus_2_2_is_4 [lemma, in LF.Logic]
Poly [library]
Postscript [library]
Preface [library]
preorder [definition, in LF.Rel]
primary [constructor, in LF.Basics]
prod [inductive, in LF.Poly]
proj1 [lemma, in LF.Logic]
proj2 [lemma, in LF.Logic]
ProofObjects [library]
Props [module, in LF.ProofObjects]
Props.And [module, in LF.ProofObjects]
Props.And.and [inductive, in LF.ProofObjects]
Props.And.conj [constructor, in LF.ProofObjects]
Props.and_comm [lemma, in LF.ProofObjects]
Props.and_comm' [definition, in LF.ProofObjects]
Props.and_comm'_aux [definition, in LF.ProofObjects]
Props.conj_fact [definition, in LF.ProofObjects]
Props.Ex [module, in LF.ProofObjects]
Props.Ex.ex [inductive, in LF.ProofObjects]
Props.Ex.ex_intro [constructor, in LF.ProofObjects]
Props.ex_ev_Sn [definition, in LF.ProofObjects]
Props.False [inductive, in LF.ProofObjects]
Props.I [constructor, in LF.ProofObjects]
Props.Or [module, in LF.ProofObjects]
Props.Or.or [inductive, in LF.ProofObjects]
Props.Or.or_introl [constructor, in LF.ProofObjects]
Props.Or.or_intror [constructor, in LF.ProofObjects]
Props.or_comm [definition, in LF.ProofObjects]
Props.some_nat_is_even [definition, in LF.ProofObjects]
Props.True [inductive, in LF.ProofObjects]
provable_equiv_true [lemma, in LF.IndProp]
Pumping [module, in LF.IndProp]
Pumping.napp [definition, in LF.IndProp]
Pumping.napp_plus [lemma, in LF.IndProp]
Pumping.pumping [lemma, in LF.IndProp]
Pumping.pumping_constant [definition, in LF.IndProp]
pup_to_n [definition, in LF.Imp]
pup_to_n [definition, in LF.ImpCEvalFun]
pup_to_2_ceval [lemma, in LF.Imp]
P_m0r [definition, in LF.IndPrinciples]
P_m0r' [definition, in LF.IndPrinciples]

R

R [module, in LF.IndProp]
red [constructor, in LF.IndPrinciples]
red [constructor, in LF.Basics]
reflect [inductive, in LF.IndProp]
ReflectF [constructor, in LF.IndProp]
ReflectT [constructor, in LF.IndProp]
reflect_iff [lemma, in LF.IndProp]
reflexive [definition, in LF.Rel]
refl_matches_eps [definition, in LF.IndProp]
regex_match [definition, in LF.IndProp]
regex_refl [lemma, in LF.IndProp]
reg_exp [inductive, in LF.IndProp]
reg_exp_ex₁ [definition, in LF.IndProp]
reg_exp_ex₂ [definition, in LF.IndProp]
reg_exp_ex₃ [definition, in LF.IndProp]
reg_exp_ex₄ [definition, in LF.IndProp]
reg_exp_of_list [definition, in LF.IndProp]
reg_exp_of_list_spec [lemma, in LF.IndProp]
Rel [library]
relation [definition, in LF.Rel]
Repeat [module, in LF.Auto]
repeat [definition, in LF.Poly]
repeats [inductive, in LF.IndProp]
repeat' [definition, in LF.Poly]
repeat'' [definition, in LF.Poly]
repeat''' [definition, in LF.Poly]
Repeat.CAsgn [constructor, in LF.Auto]
Repeat.ceval [inductive, in LF.Auto]
Repeat.ceval_deterministic [lemma, in LF.Auto]
Repeat.ceval_deterministic' [lemma, in LF.Auto]
Repeat.CIf [constructor, in LF.Auto]
Repeat.com [inductive, in LF.Auto]
Repeat.CRepeat [constructor, in LF.Auto]
Repeat.CSeq [constructor, in LF.Auto]
Repeat.CSkip [constructor, in LF.Auto]
Repeat.CWhile [constructor, in LF.Auto]
Repeat.E_Ass [constructor, in LF.Auto]
Repeat.E_IfFalse [constructor, in LF.Auto]
Repeat.E_IfTrue [constructor, in LF.Auto]
Repeat.E_RepeatEnd [constructor, in LF.Auto]
Repeat.E_RepeatLoop [constructor, in LF.Auto]
Repeat.E_Seq [constructor, in LF.Auto]
Repeat.E_Skip [constructor, in LF.Auto]
Repeat.E_WhileFalse [constructor, in LF.Auto]
Repeat.E_WhileTrue [constructor, in LF.Auto]
Repeat.::x_'::='_x [notation, in LF.Auto]
Repeat.::x_';'_x [notation, in LF.Auto]
Repeat.::x_'=['_x_']=>'_x [notation, in LF.Auto]
Repeat.::'REPEAT'_x_'UNTIL'_x_'END' [notation, in LF.Auto]
Repeat.::'SKIP' [notation, in LF.Auto]
Repeat.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in LF.Auto]
Repeat.::'WHILE'_x_'DO'_x_'END' [notation, in LF.Auto]
restricted_excluded_middle [lemma, in LF.Logic]
restricted_excluded_middle_eq [lemma, in LF.Logic]
rev [definition, in LF.Poly]
rev_append [definition, in LF.Logic]
rev_app_distr [lemma, in LF.Poly]
rev_exercise1 [lemma, in LF.Tactics]
rev_involutive [lemma, in LF.Poly]
re_chars [definition, in LF.IndProp]
re_not_empty [definition, in LF.IndProp]
re_not_empty_correct [lemma, in LF.IndProp]
rgb [inductive, in LF.IndPrinciples]
rgb [inductive, in LF.Basics]
rsc_R [lemma, in LF.Rel]
rsc_trans [lemma, in LF.Rel]
rtc_rsc_coincide [lemma, in LF.Rel]
rt1n_refl [constructor, in LF.Rel]
rt1n_trans [constructor, in LF.Rel]
rt_refl [constructor, in LF.Rel]
rt_step [constructor, in LF.Rel]
rt_trans [constructor, in LF.Rel]
R.c1 [constructor, in LF.IndProp]
R.c2 [constructor, in LF.IndProp]
R.c3 [constructor, in LF.IndProp]
R.c4 [constructor, in LF.IndProp]
R.c5 [constructor, in LF.IndProp]
R.fR [definition, in LF.IndProp]
R.manual_grade_for_R_provability [definition, in LF.IndProp]
R.R [inductive, in LF.IndProp]
R.R_equiv_fR [lemma, in LF.IndProp]

S

saturday [constructor, in LF.Basics]
sillyfun [definition, in LF.Tactics]
sillyfun1 [definition, in LF.Tactics]
sillyfun1_odd [lemma, in LF.Tactics]
sillyfun1_odd_FAILED [lemma, in LF.Tactics]
sillyfun_false [lemma, in LF.Tactics]
silly1 [lemma, in LF.Tactics]
silly2 [lemma, in LF.Tactics]
silly2a [lemma, in LF.Tactics]
silly3' [lemma, in LF.Tactics]
silly3_firsttry [lemma, in LF.Tactics]
silly_ex [lemma, in LF.Tactics]
silly_fact_1 [lemma, in LF.Tactics]
silly_fact_2 [lemma, in LF.Tactics]
silly_fact_2' [lemma, in LF.Tactics]
silly_fact_2_FAILED [lemma, in LF.Tactics]
sinstr [inductive, in LF.Imp]
SLoad [constructor, in LF.Imp]
SMinus [constructor, in LF.Imp]
SMult [constructor, in LF.Imp]
snd [definition, in LF.Poly]
Sn_le_Sm__n_le_m [lemma, in LF.IndProp]
SomeE [constructor, in LF.ImpParser]
split [definition, in LF.Tactics]
split [definition, in LF.Poly]
split_combine [lemma, in LF.Tactics]
split_combine_statement [definition, in LF.Tactics]
SPlus [constructor, in LF.Imp]
SPush [constructor, in LF.Imp]
sq [constructor, in LF.IndProp]
square [definition, in LF.Tactics]
square_mult [lemma, in LF.Tactics]
square_of [inductive, in LF.IndProp]
SSSSev__even [lemma, in LF.IndProp]
Star [constructor, in LF.IndProp]
star_app [lemma, in LF.IndProp]
star_app [lemma, in LF.IndProp]
star_app [lemma, in LF.IndProp]
star_ne [lemma, in LF.IndProp]
state [definition, in LF.Imp]
string [definition, in LF.IndProp]
string_of_list [definition, in LF.ImpParser]
st₁₂ [definition, in LF.Auto]
st₂₁ [definition, in LF.Auto]
subseq [inductive, in LF.IndProp]
subseq_app [lemma, in LF.IndProp]
subseq_refl [lemma, in LF.IndProp]
subseq_trans [lemma, in LF.IndProp]
subtract_slowly [definition, in LF.Imp]
subtract_slowly_body [definition, in LF.Imp]
subtract_3_from_5_slowly [definition, in LF.Imp]
succ_inj [lemma, in LF.Logic]
sunday [constructor, in LF.Basics]
symmetric [definition, in LF.Rel]
s_compile [definition, in LF.Imp]
s_compile1 [definition, in LF.Imp]
s_compile_correct [lemma, in LF.Imp]
s_execute [definition, in LF.Imp]
s_execute1 [definition, in LF.Imp]
s_execute2 [definition, in LF.Imp]
S_inj [lemma, in LF.Tactics]
S_injective [lemma, in LF.Tactics]
S_injective' [lemma, in LF.Tactics]
S_nbeq_0 [lemma, in LF.Induction]

T

Tactics [library]
testParsing [definition, in LF.ImpParser]
test_andb31 [definition, in LF.Basics]
test_andb32 [definition, in LF.Basics]
test_andb33 [definition, in LF.Basics]
test_andb34 [definition, in LF.Basics]
test_anon_fun' [definition, in LF.Poly]
test_ceval [definition, in LF.ImpCEvalFun]
test_countoddmembers'1 [definition, in LF.Poly]
test_countoddmembers'2 [definition, in LF.Poly]
test_countoddmembers'3 [definition, in LF.Poly]
test_der0 [definition, in LF.IndProp]
test_der1 [definition, in LF.IndProp]
test_der2 [definition, in LF.IndProp]
test_der3 [definition, in LF.IndProp]
test_der4 [definition, in LF.IndProp]
test_der5 [definition, in LF.IndProp]
test_der6 [definition, in LF.IndProp]
test_der7 [definition, in LF.IndProp]
test_doit3times [definition, in LF.Poly]
test_doit3times' [definition, in LF.Poly]
test_existsb_1 [definition, in LF.Tactics]
test_existsb_2 [definition, in LF.Tactics]
test_existsb_3 [definition, in LF.Tactics]
test_existsb_4 [definition, in LF.Tactics]
test_factorial1 [definition, in LF.Basics]
test_factorial2 [definition, in LF.Basics]
test_filter1 [definition, in LF.Poly]
test_filter2 [definition, in LF.Poly]
test_filter2' [definition, in LF.Poly]
test_filter_even_gt7_1 [definition, in LF.Poly]
test_filter_even_gt7_2 [definition, in LF.Poly]
test_flat_map1 [definition, in LF.Poly]
test_forallb_1 [definition, in LF.Tactics]
test_forallb_2 [definition, in LF.Tactics]
test_forallb_3 [definition, in LF.Tactics]
test_forallb_4 [definition, in LF.Tactics]
test_hd_error1 [definition, in LF.Poly]
test_hd_error2 [definition, in LF.Poly]
test_leb1 [definition, in LF.Basics]
test_leb2 [definition, in LF.Basics]
test_leb3 [definition, in LF.Basics]
test_leb3' [definition, in LF.Basics]
test_length1 [definition, in LF.Poly]
test_ltb1 [definition, in LF.Basics]
test_ltb2 [definition, in LF.Basics]
test_ltb3 [definition, in LF.Basics]
test_map1 [definition, in LF.Poly]
test_map2 [definition, in LF.Poly]
test_map3 [definition, in LF.Poly]
test_nandb1 [definition, in LF.Basics]
test_nandb2 [definition, in LF.Basics]
test_nandb3 [definition, in LF.Basics]
test_nandb4 [definition, in LF.Basics]
test_next_weekday [definition, in LF.Basics]
test_nostutter_1 [definition, in LF.IndProp]
test_nostutter_2 [definition, in LF.IndProp]
test_nostutter_3 [definition, in LF.IndProp]
test_nostutter_4 [definition, in LF.IndProp]
test_nth_error1 [definition, in LF.Poly]
test_nth_error2 [definition, in LF.Poly]
test_nth_error3 [definition, in LF.Poly]
test_oddb1 [definition, in LF.Basics]
test_oddb2 [definition, in LF.Basics]
test_orb1 [definition, in LF.Basics]
test_orb2 [definition, in LF.Basics]
test_orb3 [definition, in LF.Basics]
test_orb4 [definition, in LF.Basics]
test_orb5 [definition, in LF.Basics]
test_partition1 [definition, in LF.Poly]
test_partition2 [definition, in LF.Poly]
test_plus3 [definition, in LF.Poly]
test_plus3' [definition, in LF.Poly]
test_plus3'' [definition, in LF.Poly]
test_repeat1 [definition, in LF.Poly]
test_repeat2 [definition, in LF.Poly]
test_rev1 [definition, in LF.Poly]
test_rev2 [definition, in LF.Poly]
test_split [definition, in LF.Poly]
thursday [constructor, in LF.Basics]
token [definition, in LF.ImpParser]
tokenize [definition, in LF.ImpParser]
tokenize_ex₁ [definition, in LF.ImpParser]
tokenize_helper [definition, in LF.ImpParser]
total_map [definition, in LF.Maps]
transitive [definition, in LF.Rel]
trans_eq [lemma, in LF.Tactics]
trans_eq_example [definition, in LF.Tactics]
trans_eq_example' [definition, in LF.Tactics]
trans_eq_exercise [definition, in LF.Tactics]
tree [inductive, in LF.IndPrinciples]
true [constructor, in LF.Basics]
True_is_true [lemma, in LF.Logic]
tr_rev [definition, in LF.Logic]
tr_rev_correct [lemma, in LF.Logic]
tuesday [constructor, in LF.Basics]
t_apply_empty [lemma, in LF.Maps]
t_empty [definition, in LF.Maps]
t_update [definition, in LF.Maps]
t_update_eq [lemma, in LF.Maps]
t_update_neq [lemma, in LF.Maps]
t_update_permute [lemma, in LF.Maps]
t_update_same [lemma, in LF.Maps]
t_update_shadow [lemma, in LF.Maps]

U

Union [constructor, in LF.IndProp]
union_disj [lemma, in LF.IndProp]
update [definition, in LF.Maps]
update_eq [lemma, in LF.Maps]
update_example1 [definition, in LF.Maps]
update_example2 [definition, in LF.Maps]
update_example3 [definition, in LF.Maps]
update_example4 [definition, in LF.Maps]
update_neq [lemma, in LF.Maps]
update_permute [lemma, in LF.Maps]
update_same [lemma, in LF.Maps]
update_shadow [lemma, in LF.Maps]

W

W [definition, in LF.Imp]
wednesday [constructor, in LF.Basics]
white [constructor, in LF.ImpParser]
white [constructor, in LF.Basics]
wrong_ev [inductive, in LF.IndProp]
wrong_ev_SS [constructor, in LF.IndProp]
wrong_ev_0 [constructor, in LF.IndProp]

X

X [definition, in LF.Imp]
XtimesYinZ [definition, in LF.Imp]

Y

Y [definition, in LF.Imp]
yes [constructor, in LF.IndPrinciples]
yesno [inductive, in LF.IndPrinciples]

Z

Z [definition, in LF.Imp]
Z [constructor, in LF.Basics]
zero_nbeq_plus_1 [lemma, in LF.Basics]
zero_nbeq_S [lemma, in LF.Induction]
zero_not_one [lemma, in LF.Logic]
zero_or_succ [lemma, in LF.Logic]

:

:imp_scope:x_'&&'_x [notation, in LF.Imp]
:imp_scope:x_'*'_x [notation, in LF.Imp]
:imp_scope:x_'+'_x [notation, in LF.Imp]
:imp_scope:x_'-'_x [notation, in LF.Imp]
:imp_scope:x_'::='_x [notation, in LF.Imp]
:imp_scope:x_';;'_x [notation, in LF.Imp]
:imp_scope:x_'<='_x [notation, in LF.Imp]
:imp_scope:x_'='_x [notation, in LF.Imp]
:imp_scope:'SKIP' [notation, in LF.Imp]
:imp_scope:'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in LF.Imp]
:imp_scope:'WHILE'_x_'DO'_x_'END' [notation, in LF.Imp]
:imp_scope:'~'_x [notation, in LF.Imp]
:nat_scope:x_'*'_x [notation, in LF.Basics]
:nat_scope:x_'*'_x [notation, in LF.Basics]
:nat_scope:x_'+'_x [notation, in LF.Basics]
:nat_scope:x_'+'_x [notation, in LF.Basics]
:nat_scope:x_'-'_x [notation, in LF.Basics]
:nat_scope:x_'<=?'_x [notation, in LF.ImpParser]
:nat_scope:x_'<=?'_x [notation, in LF.Basics]
:nat_scope:x_' [notation, in LF.Basics]
:nat_scope:x_'=?'_x [notation, in LF.Basics]
:type_scope:x_'*'_x [notation, in LF.Poly]
->'_x">::x_'!->'_x [notation, in LF.Imp]
->'_x_';'_x">::x_'!->'_x_';'_x [notation, in LF.Maps]
::x_'&&'_x [notation, in LF.Basics]
::x_'++'_x [notation, in LF.Poly]
::x_'::'_x [notation, in LF.Poly]
::x_'<'_x [notation, in LF.IndProp]
::x_'<='_x [notation, in LF.IndPrinciples]
::x_'=['_x_']=>'_x [notation, in LF.Imp]
::x_'=~'_x [notation, in LF.IndProp]
⊢>'_x">::x_'⊢>'_x [notation, in LF.Maps]
⊢>'_x_';'_x">::x_'⊢>'_x_';'_x [notation, in LF.Maps]
::x_'||'_x [notation, in LF.Basics]
::'LETOPT'_x_'<=='_x_'IN'_x [notation, in LF.ImpCEvalFun]
::'TRY'_''''_x_'<-'_x_';;'_x_'OR'_x [notation, in LF.ImpParser]
::''''_x_'<-'_x_';;'_x [notation, in LF.ImpParser]
->'_x">::'''_'''_'!->'_x [notation, in LF.Maps]
::'('_x_','_x_')' [notation, in LF.Poly]
::'['_x_';'_'..'_';'_x_']' [notation, in LF.Poly]
::'['_']' [notation, in LF.Poly]

---

Notation Index

A

aevalR_division.:type_scope:x_'\\'_x [in LF.Imp]
aevalR_extended.:type_scope:x_'\\'_x [in LF.Imp]
AExp.aevalR_first_try.:type_scope:x_'\\'_x [in LF.Imp]
AExp.:type_scope:x_'\\'_x [in LF.Imp]

B

BreakImp.::x_'::='_x [in LF.Imp]
BreakImp.::x_';;'_x [in LF.Imp]
BreakImp.::x_'=['_x_']=>'_x_'/'_x [in LF.Imp]
BreakImp.::'BREAK' [in LF.Imp]
BreakImp.::'SKIP' [in LF.Imp]
BreakImp.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in LF.Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [in LF.Imp]

M

MyEquality.:type_scope:x_'=='_x [in LF.ProofObjects]
->'_x">MyIff.:type_scope:x_'<->'_x [in LF.Logic]
MyNot.:type_scope:'~'_x [in LF.Logic]

N

NatList.::x_'++'_x [in LF.Lists]
NatList.::x_'::'_x [in LF.Lists]
NatList.::'('_x_','_x_')' [in LF.Lists]
NatList.::'['_x_';'_'..'_';'_x_']' [in LF.Lists]
NatList.::'['_']' [in LF.Lists]

P

Playground.::x_'<='_x [in LF.IndProp]

R

Repeat.::x_'::='_x [in LF.Auto]
Repeat.::x_';'_x [in LF.Auto]
Repeat.::x_'=['_x_']=>'_x [in LF.Auto]
Repeat.::'REPEAT'_x_'UNTIL'_x_'END' [in LF.Auto]
Repeat.::'SKIP' [in LF.Auto]
Repeat.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in LF.Auto]
Repeat.::'WHILE'_x_'DO'_x_'END' [in LF.Auto]

:

:imp_scope:x_'&&'_x [in LF.Imp]
:imp_scope:x_'*'_x [in LF.Imp]
:imp_scope:x_'+'_x [in LF.Imp]
:imp_scope:x_'-'_x [in LF.Imp]
:imp_scope:x_'::='_x [in LF.Imp]
:imp_scope:x_';;'_x [in LF.Imp]
:imp_scope:x_'<='_x [in LF.Imp]
:imp_scope:x_'='_x [in LF.Imp]
:imp_scope:'SKIP' [in LF.Imp]
:imp_scope:'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in LF.Imp]
:imp_scope:'WHILE'_x_'DO'_x_'END' [in LF.Imp]
:imp_scope:'~'_x [in LF.Imp]
:nat_scope:x_'*'_x [in LF.Basics]
:nat_scope:x_'*'_x [in LF.Basics]
:nat_scope:x_'+'_x [in LF.Basics]
:nat_scope:x_'+'_x [in LF.Basics]
:nat_scope:x_'-'_x [in LF.Basics]
:nat_scope:x_'<=?'_x [in LF.ImpParser]
:nat_scope:x_'<=?'_x [in LF.Basics]
:nat_scope:x_' [in LF.Basics]
:nat_scope:x_'=?'_x [in LF.Basics]
:type_scope:x_'*'_x [in LF.Poly]
->'_x">::x_'!->'_x [in LF.Imp]
->'_x_';'_x">::x_'!->'_x_';'_x [in LF.Maps]
::x_'&&'_x [in LF.Basics]
::x_'++'_x [in LF.Poly]
::x_'::'_x [in LF.Poly]
::x_'<'_x [in LF.IndProp]
::x_'<='_x [in LF.IndPrinciples]
::x_'=['_x_']=>'_x [in LF.Imp]
::x_'=~'_x [in LF.IndProp]
⊢>'_x">::x_'⊢>'_x [in LF.Maps]
⊢>'_x_';'_x">::x_'⊢>'_x_';'_x [in LF.Maps]
::x_'||'_x [in LF.Basics]
::'LETOPT'_x_'<=='_x_'IN'_x [in LF.ImpCEvalFun]
::'TRY'_''''_x_'<-'_x_';;'_x_'OR'_x [in LF.ImpParser]
::''''_x_'<-'_x_';;'_x [in LF.ImpParser]
->'_x">::'''_'''_'!->'_x [in LF.Maps]
::'('_x_','_x_')' [in LF.Poly]
::'['_x_';'_'..'_';'_x_']' [in LF.Poly]
::'['_']' [in LF.Poly]

---

Module Index

A

aevalR_division [in LF.Imp]
aevalR_extended [in LF.Imp]
AExp [in LF.Imp]
AExp.aevalR_first_try [in LF.Imp]
AExp.aevalR_first_try.TooHardToRead [in LF.Imp]

B

BreakImp [in LF.Imp]

E

Exercises [in LF.Poly]
Exercises.Church [in LF.Poly]

M

MumbleGrumble [in LF.Poly]
MyEquality [in LF.ProofObjects]
MyIff [in LF.Logic]
MyNot [in LF.Logic]

N

NatList [in LF.Lists]
NatPlayground [in LF.Basics]
NatPlayground2 [in LF.Basics]

O

OptionPlayground [in LF.Poly]

P

PartialMap [in LF.Lists]
Playground [in LF.IndProp]
Props [in LF.ProofObjects]
Props.And [in LF.ProofObjects]
Props.Ex [in LF.ProofObjects]
Props.Or [in LF.ProofObjects]
Pumping [in LF.IndProp]

R

R [in LF.IndProp]
Repeat [in LF.Auto]

---

Library Index

A

Auto

B

Basics
Bib

E

Extraction

I

Imp
ImpCEvalFun
ImpParser
IndPrinciples
IndProp
Induction

L

Lists
Logic

M

Maps

P

Poly
Postscript
Preface
ProofObjects

R

Rel

T

Tactics

---

Lemma Index

A

AExp.aeval_iff_aevalR [in LF.Imp]
AExp.aeval_iff_aevalR' [in LF.Imp]
AExp.beval_iff_bevalR [in LF.Imp]
AExp.foo [in LF.Imp]
AExp.foo' [in LF.Imp]
AExp.In10 [in LF.Imp]
AExp.In10' [in LF.Imp]
AExp.optimize_0plus_b_sound [in LF.Imp]
AExp.optimize_0plus_sound [in LF.Imp]
AExp.optimize_0plus_sound' [in LF.Imp]
AExp.optimize_0plus_sound'' [in LF.Imp]
AExp.silly1 [in LF.Imp]
AExp.silly2 [in LF.Imp]
all3_spec [in LF.Induction]
All_In [in LF.Logic]
andb3_exchange [in LF.Basics]
andb_commutative [in LF.Basics]
andb_commutative' [in LF.Basics]
andb_commutative'' [in LF.Basics]
andb_eq_orb [in LF.Basics]
andb_false_r [in LF.Induction]
andb_true_elim2 [in LF.Basics]
andb_true_iff [in LF.Logic]
and_assoc [in LF.Logic]
and_commut [in LF.Logic]
and_example2 [in LF.Logic]
and_example2' [in LF.Logic]
and_example2'' [in LF.Logic]
and_example3 [in LF.Logic]
and_intro [in LF.Logic]
apply_empty [in LF.Maps]
apply_iff_example [in LF.Logic]
app_assoc [in LF.Poly]
app_exists [in LF.IndProp]
app_length [in LF.Poly]
app_ne [in LF.IndProp]
app_nil_r [in LF.Poly]

B

bool_fn_applied_thrice [in LF.Tactics]
BreakImp.break_ignore [in LF.Imp]
BreakImp.ceval_deterministic [in LF.Imp]
BreakImp.while_break_true [in LF.Imp]
BreakImp.while_continue [in LF.Imp]
BreakImp.while_stops_on_break [in LF.Imp]

C

ceval_and_ceval_step_coincide [in LF.ImpCEvalFun]
ceval_deterministic [in LF.Auto]
ceval_deterministic [in LF.Imp]
ceval_deterministic' [in LF.ImpCEvalFun]
ceval_deterministic' [in LF.Auto]
ceval_deterministic'' [in LF.Auto]
ceval_deterministic''' [in LF.Auto]
ceval_deterministic'''' [in LF.Auto]
ceval_deterministic''''' [in LF.Auto]
ceval_deterministic'_alt [in LF.Auto]
ceval_step_more [in LF.ImpCEvalFun]
ceval_step__ceval [in LF.ImpCEvalFun]
ceval__ceval_step [in LF.ImpCEvalFun]
char_eps_suffix [in LF.IndProp]
char_nomatch_char [in LF.IndProp]
combine_odd_even_elim_even [in LF.Logic]
combine_odd_even_elim_odd [in LF.Logic]
combine_odd_even_intro [in LF.Logic]
combine_split [in LF.Tactics]
contradiction_implies_anything [in LF.Logic]
contrapositive [in LF.Logic]

D

derive_corr [in LF.IndProp]
discriminate_ex₁ [in LF.Tactics]
discriminate_ex₂ [in LF.Tactics]
dist_exists_or [in LF.Logic]
dist_not_exists [in LF.Logic]
double_injective [in LF.Tactics]
double_injective_FAILED [in LF.Tactics]
double_injective_take2 [in LF.Tactics]
double_injective_take2_FAILED [in LF.Tactics]
double_neg [in LF.Logic]
double_plus [in LF.Induction]

E

empty_is_empty [in LF.IndProp]
empty_matches_eps [in LF.IndProp]
empty_nomatch_ne [in LF.IndProp]
eqbP [in LF.IndProp]
eqbP_practice [in LF.IndProp]
eqb_eq [in LF.Logic]
eqb_id_refl [in LF.Lists]
eqb_id_true [in LF.Tactics]
eqb_list_true_iff [in LF.Logic]
eqb_neq [in LF.Logic]
eqb_refl [in LF.Induction]
eqb_stringP [in LF.Maps]
eqb_string_false_iff [in LF.Maps]
eqb_string_refl [in LF.Maps]
eqb_string_true_iff [in LF.Maps]
eqb_sym [in LF.Tactics]
eqb_trans [in LF.Tactics]
eqb_true [in LF.Tactics]
eqb_0_l [in LF.Tactics]
evenb_double [in LF.Logic]
evenb_double_conv [in LF.Logic]
evenb_S [in LF.Induction]
even'_ev [in LF.IndProp]
even5_nonsense [in LF.IndProp]
even_bool_prop [in LF.Logic]
evSS_ev [in LF.IndProp]
evSS_ev [in LF.IndProp]
evSS_ev' [in LF.IndProp]
ev_double [in LF.IndProp]
ev_even [in LF.IndProp]
ev_even_firsttry [in LF.IndProp]
ev_even_iff [in LF.IndProp]
ev_ev' [in LF.IndPrinciples]
ev_ev__ev [in LF.IndProp]
ev_inversion [in LF.IndProp]
ev_minus2 [in LF.IndProp]
ev_plus4 [in LF.ProofObjects]
ev_plus4 [in LF.IndProp]
ev_plus_plus [in LF.IndProp]
ev_sum [in LF.IndProp]
ev_4 [in LF.ProofObjects]
ev_4 [in LF.IndProp]
ev_4' [in LF.IndProp]
ev_4' [in LF.ProofObjects]
ev_4'' [in LF.ProofObjects]
ev_8 [in LF.ProofObjects]
excluded_middle_irrefutable [in LF.Logic]
Exercises.curry_uncurry [in LF.Poly]
Exercises.fold_length_correct [in LF.Poly]
Exercises.uncurry_curry [in LF.Poly]
existsb_existsb' [in LF.Tactics]
exists_example_2 [in LF.Logic]
ex_falso_quodlibet [in LF.Logic]

F

false_eqb_string [in LF.Maps]
filter_exercise [in LF.Tactics]
filter_not_empty_In [in LF.IndProp]
filter_not_empty_In' [in LF.IndProp]
forallb_true_iff [in LF.Logic]
four_is_even [in LF.Logic]
f_equal [in LF.Tactics]

I

identity_fn_applied_twice [in LF.Basics]
iff_refl [in LF.Logic]
iff_reflect [in LF.IndProp]
iff_sym [in LF.Logic]
iff_trans [in LF.Logic]
injection_ex₁ [in LF.Tactics]
injection_ex₂ [in LF.Tactics]
inversion_ex₁ [in LF.IndProp]
inversion_ex₂ [in LF.IndProp]
In_app_iff [in LF.Logic]
In_map [in LF.Logic]
In_map_iff [in LF.Logic]
in_not_nil [in LF.Logic]
in_not_nil_42 [in LF.Logic]
in_not_nil_42_take2 [in LF.Logic]
in_not_nil_42_take3 [in LF.Logic]
in_not_nil_42_take4 [in LF.Logic]
in_not_nil_42_take5 [in LF.Logic]
in_re_match [in LF.IndProp]
in_split [in LF.IndProp]

L

leb_complete [in LF.IndProp]
leb_correct [in LF.IndProp]
leb_iff [in LF.IndProp]
leb_refl [in LF.Induction]
leb_true_trans [in LF.IndProp]
le_antisym [in LF.Auto]
le_antisymmetric [in LF.Rel]
le_not_a_partial_function [in LF.Rel]
le_not_symmetric [in LF.Rel]
le_order [in LF.Rel]
le_plus_l [in LF.IndProp]
le_reflexive [in LF.Rel]
le_Sn_le [in LF.Rel]
le_Sn_n [in LF.Rel]
le_step [in LF.Rel]
le_S_n [in LF.Rel]
le_trans [in LF.IndProp]
le_trans [in LF.Rel]
loop_never_stops [in LF.Imp]
lt_S [in LF.IndProp]
lt_trans [in LF.Rel]
lt_trans' [in LF.Rel]
lt_trans'' [in LF.Rel]

M

map_rev [in LF.Poly]
match_eps_refl [in LF.IndProp]
minus_diag [in LF.Induction]
MStar' [in LF.IndProp]
MStar'' [in LF.IndProp]
MStar1 [in LF.IndProp]
mult_assoc [in LF.Induction]
mult_comm [in LF.Induction]
mult_eq_0 [in LF.Logic]
mult_plus_distr_r [in LF.Induction]
mult_S_1 [in LF.Basics]
mult_0 [in LF.Logic]
mult_0_l [in LF.Basics]
mult_0_plus [in LF.Basics]
mult_0_plus' [in LF.Induction]
mult_0_r [in LF.Induction]
mult_0_r' [in LF.IndPrinciples]
mult_0_r'' [in LF.IndPrinciples]
mult_0_3 [in LF.Logic]
mult_1_l [in LF.Induction]
MUnion' [in LF.IndProp]
MyEquality.equality__leibniz_equality [in LF.ProofObjects]
MyEquality.four [in LF.ProofObjects]
MyEquality.leibniz_equality__equality [in LF.ProofObjects]

N

NatList.app_assoc [in LF.Lists]
NatList.app_assoc4 [in LF.Lists]
NatList.app_length [in LF.Lists]
NatList.app_nil_r [in LF.Lists]
NatList.count_member_nonzero [in LF.Lists]
NatList.eqblist_refl [in LF.Lists]
NatList.fst_swap_is_snd [in LF.Lists]
NatList.leb_n_Sn [in LF.Lists]
NatList.nil_app [in LF.Lists]
NatList.nonzeros_app [in LF.Lists]
NatList.option_elim_hd [in LF.Lists]
NatList.remove_does_not_increase_count [in LF.Lists]
NatList.rev_app_distr [in LF.Lists]
NatList.rev_involutive [in LF.Lists]
NatList.rev_length [in LF.Lists]
NatList.rev_length_firsttry [in LF.Lists]
NatList.snd_fst_is_swap [in LF.Lists]
NatList.surjective_pairing [in LF.Lists]
NatList.surjective_pairing' [in LF.Lists]
NatList.surjective_pairing_stuck [in LF.Lists]
NatList.tl_length_pred [in LF.Lists]
nat_bin_nat [in LF.Induction]
negb_involutive [in LF.Basics]
next_nat_closure_is_le [in LF.Rel]
next_nat_partial_function [in LF.Rel]
not_both_true_and_false [in LF.Logic]
not_equiv_false [in LF.IndProp]
not_exists_dist [in LF.Logic]
not_False [in LF.Logic]
not_implies_our_not [in LF.Logic]
not_true_iff_false [in LF.Logic]
not_true_is_false [in LF.Logic]
not_true_is_false' [in LF.Logic]
no_whiles_eqv [in LF.Imp]
nth_error_after_last [in LF.Tactics]
null_matches_none [in LF.IndProp]
n_le_m__Sn_le_Sm [in LF.IndProp]

O

one_not_even [in LF.IndProp]
one_not_even' [in LF.IndProp]
orb_true_iff [in LF.Logic]
or_assoc [in LF.Logic]
or_commut [in LF.Logic]
or_distributes_over_and [in LF.Logic]
or_example [in LF.Logic]
or_intro [in LF.Logic]
O_le_n [in LF.IndProp]

P

PartialMap.update_eq [in LF.Lists]
PartialMap.update_neq [in LF.Lists]
pigeonhole_principle [in LF.IndProp]
Playground.test_le₁ [in LF.IndProp]
Playground.test_le₂ [in LF.IndProp]
Playground.test_le₃ [in LF.IndProp]
plus2_spec [in LF.Imp]
plus_assoc [in LF.Induction]
plus_assoc' [in LF.Induction]
plus_assoc' [in LF.IndPrinciples]
plus_assoc'' [in LF.Induction]
plus_ble_compat_l [in LF.Induction]
plus_comm [in LF.Induction]
plus_comm' [in LF.IndPrinciples]
plus_comm'' [in LF.IndPrinciples]
plus_comm3 [in LF.Logic]
plus_comm3_take2 [in LF.Logic]
plus_comm3_take3 [in LF.Logic]
plus_eqb_example [in LF.Logic]
plus_fact_is_true [in LF.Logic]
plus_id_example [in LF.Basics]
plus_id_exercise [in LF.Basics]
plus_lt [in LF.IndProp]
plus_n_n_injective [in LF.Tactics]
plus_n_O [in LF.Induction]
plus_n_O_firsttry [in LF.Induction]
plus_n_O_secondtry [in LF.Induction]
plus_n_Sm [in LF.Induction]
plus_one_r' [in LF.IndPrinciples]
plus_O_n [in LF.Basics]
plus_O_n' [in LF.Basics]
plus_rearrange [in LF.Induction]
plus_rearrange_firsttry [in LF.Induction]
plus_swap [in LF.Induction]
plus_swap' [in LF.Induction]
plus_1_l [in LF.Basics]
plus_1_neq_0 [in LF.Basics]
plus_1_neq_0' [in LF.Basics]
plus_1_neq_0_firsttry [in LF.Basics]
plus_2_2_is_4 [in LF.Logic]
proj1 [in LF.Logic]
proj2 [in LF.Logic]
Props.and_comm [in LF.ProofObjects]
provable_equiv_true [in LF.IndProp]
Pumping.napp_plus [in LF.IndProp]
Pumping.pumping [in LF.IndProp]
pup_to_2_ceval [in LF.Imp]

R

reflect_iff [in LF.IndProp]
regex_refl [in LF.IndProp]
reg_exp_of_list_spec [in LF.IndProp]
Repeat.ceval_deterministic [in LF.Auto]
Repeat.ceval_deterministic' [in LF.Auto]
restricted_excluded_middle [in LF.Logic]
restricted_excluded_middle_eq [in LF.Logic]
rev_app_distr [in LF.Poly]
rev_exercise1 [in LF.Tactics]
rev_involutive [in LF.Poly]
re_not_empty_correct [in LF.IndProp]
rsc_R [in LF.Rel]
rsc_trans [in LF.Rel]
rtc_rsc_coincide [in LF.Rel]
R.R_equiv_fR [in LF.IndProp]

S

sillyfun1_odd [in LF.Tactics]
sillyfun1_odd_FAILED [in LF.Tactics]
sillyfun_false [in LF.Tactics]
silly1 [in LF.Tactics]
silly2 [in LF.Tactics]
silly2a [in LF.Tactics]
silly3' [in LF.Tactics]
silly3_firsttry [in LF.Tactics]
silly_ex [in LF.Tactics]
silly_fact_1 [in LF.Tactics]
silly_fact_2 [in LF.Tactics]
silly_fact_2' [in LF.Tactics]
silly_fact_2_FAILED [in LF.Tactics]
Sn_le_Sm__n_le_m [in LF.IndProp]
split_combine [in LF.Tactics]
square_mult [in LF.Tactics]
SSSSev__even [in LF.IndProp]
star_app [in LF.IndProp]
star_app [in LF.IndProp]
star_app [in LF.IndProp]
star_ne [in LF.IndProp]
subseq_app [in LF.IndProp]
subseq_refl [in LF.IndProp]
subseq_trans [in LF.IndProp]
succ_inj [in LF.Logic]
s_compile_correct [in LF.Imp]
S_inj [in LF.Tactics]
S_injective [in LF.Tactics]
S_injective' [in LF.Tactics]
S_nbeq_0 [in LF.Induction]

T

trans_eq [in LF.Tactics]
True_is_true [in LF.Logic]
tr_rev_correct [in LF.Logic]
t_apply_empty [in LF.Maps]
t_update_eq [in LF.Maps]
t_update_neq [in LF.Maps]
t_update_permute [in LF.Maps]
t_update_same [in LF.Maps]
t_update_shadow [in LF.Maps]

U

union_disj [in LF.IndProp]
update_eq [in LF.Maps]
update_neq [in LF.Maps]
update_permute [in LF.Maps]
update_same [in LF.Maps]
update_shadow [in LF.Maps]

Z

zero_nbeq_plus_1 [in LF.Basics]
zero_nbeq_S [in LF.Induction]
zero_not_one [in LF.Logic]
zero_or_succ [in LF.Logic]

---

Constructor Index

A

A [in LF.Basics]
aevalR_division.ADiv [in LF.Imp]
aevalR_division.AMinus [in LF.Imp]
aevalR_division.AMult [in LF.Imp]
aevalR_division.ANum [in LF.Imp]
aevalR_division.APlus [in LF.Imp]
aevalR_division.E_ADiv [in LF.Imp]
aevalR_division.E_AMinus [in LF.Imp]
aevalR_division.E_AMult [in LF.Imp]
aevalR_division.E_ANum [in LF.Imp]
aevalR_division.E_APlus [in LF.Imp]
aevalR_extended.AAny [in LF.Imp]
aevalR_extended.AMinus [in LF.Imp]
aevalR_extended.AMult [in LF.Imp]
aevalR_extended.ANum [in LF.Imp]
aevalR_extended.APlus [in LF.Imp]
aevalR_extended.E_AMinus [in LF.Imp]
aevalR_extended.E_AMult [in LF.Imp]
aevalR_extended.E_ANum [in LF.Imp]
aevalR_extended.E_Any [in LF.Imp]
aevalR_extended.E_APlus [in LF.Imp]
AExp.aevalR_first_try.E_AMinus [in LF.Imp]
AExp.aevalR_first_try.E_AMult [in LF.Imp]
AExp.aevalR_first_try.E_ANum [in LF.Imp]
AExp.aevalR_first_try.E_APlus [in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_AMinus [in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_AMult [in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_ANum [in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.E_APlus [in LF.Imp]
AExp.AMinus [in LF.Imp]
AExp.AMult [in LF.Imp]
AExp.ANum [in LF.Imp]
AExp.APlus [in LF.Imp]
AExp.BAnd [in LF.Imp]
AExp.BEq [in LF.Imp]
AExp.BFalse [in LF.Imp]
AExp.BLe [in LF.Imp]
AExp.BNot [in LF.Imp]
AExp.BTrue [in LF.Imp]
AExp.E_AMinus [in LF.Imp]
AExp.E_AMult [in LF.Imp]
AExp.E_ANum [in LF.Imp]
AExp.E_APlus [in LF.Imp]
AId [in LF.Imp]
alpha [in LF.ImpParser]
AMinus [in LF.Imp]
AMult [in LF.Imp]
ANum [in LF.Imp]
APlus [in LF.Imp]
App [in LF.IndProp]

B

B [in LF.Basics]
BAnd [in LF.Imp]
Baz1 [in LF.Lists]
Baz2 [in LF.Lists]
bempty [in LF.IndPrinciples]
BEq [in LF.Imp]
BFalse [in LF.Imp]
bits [in LF.Basics]
black [in LF.Basics]
BLe [in LF.Imp]
bleaf [in LF.IndPrinciples]
blue [in LF.Basics]
blue [in LF.IndPrinciples]
BNot [in LF.Imp]
bool_cons [in LF.Poly]
bool_nil [in LF.Poly]
BreakImp.CAss [in LF.Imp]
BreakImp.CBreak [in LF.Imp]
BreakImp.CIf [in LF.Imp]
BreakImp.CSeq [in LF.Imp]
BreakImp.CSkip [in LF.Imp]
BreakImp.CWhile [in LF.Imp]
BreakImp.E_Skip [in LF.Imp]
BreakImp.SBreak [in LF.Imp]
BreakImp.SContinue [in LF.Imp]
BTrue [in LF.Imp]
B₀ [in LF.Basics]
B₁ [in LF.Basics]

C

CAss [in LF.Imp]
Char [in LF.IndProp]
CIf [in LF.Imp]
cons [in LF.Poly]
cons' [in LF.Poly]
CSeq [in LF.Imp]
CSkip [in LF.Imp]
CWhile [in LF.Imp]
C₁ [in LF.IndPrinciples]
C₂ [in LF.IndPrinciples]

D

digit [in LF.ImpParser]

E

EmptySet [in LF.IndProp]
EmptyStr [in LF.IndProp]
even'_sum [in LF.IndProp]
even'_0 [in LF.IndProp]
even'_2 [in LF.IndProp]
ev_SS [in LF.IndProp]
ev_0 [in LF.IndProp]
E_Ass [in LF.Imp]
E_IfFalse [in LF.Imp]
E_IfTrue [in LF.Imp]
E_Seq [in LF.Imp]
E_Skip [in LF.Imp]
E_WhileFalse [in LF.Imp]
E_WhileTrue [in LF.Imp]

F

false [in LF.Basics]
friday [in LF.Basics]

G

green [in LF.Basics]
green [in LF.IndPrinciples]

I

Id [in LF.Lists]

L

leaf [in LF.IndPrinciples]
le_n [in LF.IndPrinciples]
le_S [in LF.IndPrinciples]

M

MApp [in LF.IndProp]
MChar [in LF.IndProp]
MEmpty [in LF.IndProp]
monday [in LF.Basics]
MStarApp [in LF.IndProp]
MStar0 [in LF.IndProp]
MumbleGrumble.a [in LF.Poly]
MumbleGrumble.b [in LF.Poly]
MumbleGrumble.c [in LF.Poly]
MumbleGrumble.d [in LF.Poly]
MumbleGrumble.e [in LF.Poly]
MUnionL [in LF.IndProp]
MUnionR [in LF.IndProp]
MyEquality.eq_refl [in LF.ProofObjects]

N

NatList.cons [in LF.Lists]
NatList.nil [in LF.Lists]
NatList.None [in LF.Lists]
NatList.pair [in LF.Lists]
NatList.Some [in LF.Lists]
NatPlayground.O [in LF.Basics]
NatPlayground.S [in LF.Basics]
NatPlayground.stop [in LF.Basics]
NatPlayground.tick [in LF.Basics]
nbranch [in LF.IndPrinciples]
ncons [in LF.IndPrinciples]
ne_1 [in LF.IndProp]
ne_2 [in LF.IndProp]
nil [in LF.Poly]
nil' [in LF.Poly]
nn [in LF.IndProp]
nnil [in LF.IndPrinciples]
nnil1 [in LF.IndPrinciples]
no [in LF.IndPrinciples]
node [in LF.IndPrinciples]
NoneE [in LF.ImpParser]
nsnoc1 [in LF.IndPrinciples]

O

OptionPlayground.None [in LF.Poly]
OptionPlayground.Some [in LF.Poly]
other [in LF.ImpParser]

P

pair [in LF.Poly]
PartialMap.empty [in LF.Lists]
PartialMap.record [in LF.Lists]
Playground.le_n [in LF.IndProp]
Playground.le_S [in LF.IndProp]
primary [in LF.Basics]
Props.And.conj [in LF.ProofObjects]
Props.Ex.ex_intro [in LF.ProofObjects]
Props.I [in LF.ProofObjects]
Props.Or.or_introl [in LF.ProofObjects]
Props.Or.or_intror [in LF.ProofObjects]

R

red [in LF.IndPrinciples]
red [in LF.Basics]
ReflectF [in LF.IndProp]
ReflectT [in LF.IndProp]
Repeat.CAsgn [in LF.Auto]
Repeat.CIf [in LF.Auto]
Repeat.CRepeat [in LF.Auto]
Repeat.CSeq [in LF.Auto]
Repeat.CSkip [in LF.Auto]
Repeat.CWhile [in LF.Auto]
Repeat.E_Ass [in LF.Auto]
Repeat.E_IfFalse [in LF.Auto]
Repeat.E_IfTrue [in LF.Auto]
Repeat.E_RepeatEnd [in LF.Auto]
Repeat.E_RepeatLoop [in LF.Auto]
Repeat.E_Seq [in LF.Auto]
Repeat.E_Skip [in LF.Auto]
Repeat.E_WhileFalse [in LF.Auto]
Repeat.E_WhileTrue [in LF.Auto]
rt1n_refl [in LF.Rel]
rt1n_trans [in LF.Rel]
rt_refl [in LF.Rel]
rt_step [in LF.Rel]
rt_trans [in LF.Rel]
R.c1 [in LF.IndProp]
R.c2 [in LF.IndProp]
R.c3 [in LF.IndProp]
R.c4 [in LF.IndProp]
R.c5 [in LF.IndProp]

S

saturday [in LF.Basics]
SLoad [in LF.Imp]
SMinus [in LF.Imp]
SMult [in LF.Imp]
SomeE [in LF.ImpParser]
SPlus [in LF.Imp]
SPush [in LF.Imp]
sq [in LF.IndProp]
Star [in LF.IndProp]
sunday [in LF.Basics]

T

thursday [in LF.Basics]
true [in LF.Basics]
tuesday [in LF.Basics]

U

Union [in LF.IndProp]

W

wednesday [in LF.Basics]
white [in LF.ImpParser]
white [in LF.Basics]
wrong_ev_SS [in LF.IndProp]
wrong_ev_0 [in LF.IndProp]

Y

yes [in LF.IndPrinciples]

Z

Z [in LF.Basics]

---

Axiom Index

F

functional_extensionality [in LF.Logic]

---

Inductive Index

A

aevalR_division.aevalR [in LF.Imp]
aevalR_division.aexp [in LF.Imp]
aevalR_extended.aevalR [in LF.Imp]
aevalR_extended.aexp [in LF.Imp]
aexp [in LF.Imp]
AExp.aevalR [in LF.Imp]
AExp.aevalR_first_try.aevalR [in LF.Imp]
AExp.aevalR_first_try.TooHardToRead.aevalR [in LF.Imp]
AExp.aexp [in LF.Imp]
AExp.bevalR [in LF.Imp]
AExp.bexp [in LF.Imp]

B

baz [in LF.Lists]
bexp [in LF.Imp]
bin [in LF.Basics]
bit [in LF.Basics]
bool [in LF.Basics]
boollist [in LF.Poly]
BreakImp.ceval [in LF.Imp]
BreakImp.com [in LF.Imp]
BreakImp.result [in LF.Imp]
byntree [in LF.IndPrinciples]

C

ceval [in LF.Imp]
chartype [in LF.ImpParser]
clos_refl_trans [in LF.Rel]
clos_refl_trans_1n [in LF.Rel]
color [in LF.Basics]
com [in LF.Imp]

D

day [in LF.Basics]

E

even [in LF.IndProp]
even' [in LF.IndProp]
exp_match [in LF.IndProp]
ExSet [in LF.IndPrinciples]

F

foo' [in LF.IndPrinciples]

I

id [in LF.Lists]

L

le [in LF.IndPrinciples]
list [in LF.Poly]
list' [in LF.Poly]

M

MumbleGrumble.grumble [in LF.Poly]
MumbleGrumble.mumble [in LF.Poly]
MyEquality.eq [in LF.ProofObjects]

N

natlist [in LF.IndPrinciples]
NatList.natlist [in LF.Lists]
NatList.natoption [in LF.Lists]
NatList.natprod [in LF.Lists]
natlist1 [in LF.IndPrinciples]
NatPlayground.nat [in LF.Basics]
NatPlayground.nat' [in LF.Basics]
next_even [in LF.IndProp]
next_nat [in LF.IndProp]
nostutter [in LF.IndProp]
no_whilesR [in LF.Imp]
nybble [in LF.Basics]

O

optionE [in LF.ImpParser]
OptionPlayground.option [in LF.Poly]

P

PartialMap.partial_map [in LF.Lists]
Playground.le [in LF.IndProp]
prod [in LF.Poly]
Props.And.and [in LF.ProofObjects]
Props.Ex.ex [in LF.ProofObjects]
Props.False [in LF.ProofObjects]
Props.Or.or [in LF.ProofObjects]
Props.True [in LF.ProofObjects]

R

reflect [in LF.IndProp]
reg_exp [in LF.IndProp]
repeats [in LF.IndProp]
Repeat.ceval [in LF.Auto]
Repeat.com [in LF.Auto]
rgb [in LF.IndPrinciples]
rgb [in LF.Basics]
R.R [in LF.IndProp]

S

sinstr [in LF.Imp]
square_of [in LF.IndProp]
subseq [in LF.IndProp]

T

tree [in LF.IndPrinciples]

W

wrong_ev [in LF.IndProp]

Y

yesno [in LF.IndPrinciples]

---

Definition Index

A

add1 [in LF.ProofObjects]
aeval [in LF.Imp]
AExp.aeval [in LF.Imp]
AExp.beval [in LF.Imp]
AExp.manual_grade_for_beval_rules [in LF.Imp]
AExp.optimize_0plus [in LF.Imp]
AExp.optimize_0plus_b [in LF.Imp]
AExp.silly_presburger_example [in LF.Imp]
AExp.test_aeval1 [in LF.Imp]
AExp.test_optimize_0plus [in LF.Imp]
aexp1 [in LF.Imp]
All [in LF.Logic]
all_zero [in LF.Basics]
andb [in LF.Basics]
andb3 [in LF.Basics]
and_example [in LF.Logic]
and_example' [in LF.Logic]
and_exercise [in LF.Logic]
antisymmetric [in LF.Rel]
app [in LF.Poly]
auto_example_1 [in LF.Auto]
auto_example_1' [in LF.Auto]
auto_example_2 [in LF.Auto]
auto_example_3 [in LF.Auto]
auto_example_4 [in LF.Auto]
auto_example_6 [in LF.Auto]
auto_example_6' [in LF.Auto]
auto_example_7 [in LF.Auto]
auto_example_7' [in LF.Auto]

B

bar [in LF.Tactics]
beval [in LF.Imp]
bexp1 [in LF.Imp]
bignumber [in LF.ImpParser]
bin_to_nat [in LF.Basics]
bool_to_bexp [in LF.Imp]

C

c [in LF.IndProp]
ceval'_example1 [in LF.Auto]
ceval_example1 [in LF.Auto]
ceval_example1 [in LF.Imp]
ceval_example2 [in LF.Imp]
ceval_fun_no_while [in LF.Imp]
ceval_step [in LF.ImpCEvalFun]
ceval_step1 [in LF.ImpCEvalFun]
ceval_step2 [in LF.ImpCEvalFun]
ceval_step3 [in LF.ImpCEvalFun]
classifyChar [in LF.ImpParser]
combine [in LF.Poly]
combine_odd_even [in LF.Logic]
constfun [in LF.Poly]
constfun_example1 [in LF.Poly]
constfun_example2 [in LF.Poly]
count [in LF.IndProp]
countoddmembers' [in LF.Poly]

D

d [in LF.IndProp]
derive [in LF.IndProp]
derives [in LF.IndProp]
de_morgan_not_and_not [in LF.Logic]
discriminate_ex₃ [in LF.Tactics]
doit3times [in LF.Poly]
double [in LF.Induction]
double_negation_elimination [in LF.Logic]

E

eauto_example [in LF.Auto]
eg₁ [in LF.ImpParser]
eg₂ [in LF.ImpParser]
empty [in LF.Maps]
empty_st [in LF.Imp]
eqb [in LF.Basics]
eqb_id [in LF.Lists]
eqb_list [in LF.Logic]
eqb_string [in LF.Maps]
equivalence [in LF.Rel]
evenb [in LF.Basics]
even_1000 [in LF.Logic]
even_1000' [in LF.Logic]
even_1000'' [in LF.Logic]
even_42_bool [in LF.Logic]
even_42_prop [in LF.Logic]
ev_plus2 [in LF.ProofObjects]
ev_plus2' [in LF.ProofObjects]
ev_plus2'' [in LF.ProofObjects]
ev_plus4' [in LF.ProofObjects]
ev_plus4'' [in LF.ProofObjects]
ev_4''' [in LF.ProofObjects]
ev_8' [in LF.ProofObjects]
examplemap [in LF.Maps]
examplemap' [in LF.Maps]
examplepmap [in LF.Maps]
example_aexp [in LF.Imp]
example_bexp [in LF.Imp]
example_empty [in LF.Maps]
excluded_middle [in LF.Logic]
Exercises.Church.cnat [in LF.Poly]
Exercises.Church.exp [in LF.Poly]
Exercises.Church.exp_1 [in LF.Poly]
Exercises.Church.exp_2 [in LF.Poly]
Exercises.Church.exp_3 [in LF.Poly]
Exercises.Church.mult [in LF.Poly]
Exercises.Church.mult_1 [in LF.Poly]
Exercises.Church.mult_2 [in LF.Poly]
Exercises.Church.mult_3 [in LF.Poly]
Exercises.Church.one [in LF.Poly]
Exercises.Church.plus [in LF.Poly]
Exercises.Church.plus_1 [in LF.Poly]
Exercises.Church.plus_2 [in LF.Poly]
Exercises.Church.plus_3 [in LF.Poly]
Exercises.Church.succ [in LF.Poly]
Exercises.Church.succ_1 [in LF.Poly]
Exercises.Church.succ_2 [in LF.Poly]
Exercises.Church.succ_3 [in LF.Poly]
Exercises.Church.three [in LF.Poly]
Exercises.Church.two [in LF.Poly]
Exercises.Church.zero [in LF.Poly]
Exercises.fold_length [in LF.Poly]
Exercises.fold_map [in LF.Poly]
Exercises.manual_grade_for_fold_map [in LF.Poly]
Exercises.manual_grade_for_informal_proof [in LF.Poly]
Exercises.prod_curry [in LF.Poly]
Exercises.prod_uncurry [in LF.Poly]
Exercises.test_fold_length1 [in LF.Poly]
Exercises.test_map1' [in LF.Poly]
existsb [in LF.Tactics]
existsb' [in LF.Tactics]
exp [in LF.Basics]
expect [in LF.ImpParser]

F

factorial [in LF.Basics]
fact_in_coq [in LF.Imp]
filter [in LF.Poly]
filter_even_gt₇ [in LF.Poly]
firstExpect [in LF.ImpParser]
flat_map [in LF.Poly]
fold [in LF.Poly]
fold_example1 [in LF.Poly]
fold_example2 [in LF.Poly]
fold_example3 [in LF.Poly]
foo [in LF.Tactics]
forallb [in LF.Tactics]
forallb [in LF.Logic]
fst [in LF.Poly]
ftrue [in LF.Poly]
function_equality_ex₁ [in LF.Logic]
function_equality_ex₂ [in LF.Logic]
function_equality_ex₂ [in LF.Logic]

H

hd_error [in LF.Poly]

I

implies_to_or [in LF.Logic]
In [in LF.Logic]
incr [in LF.Basics]
injection_ex₃ [in LF.Tactics]
injective [in LF.Logic]
In_example_1 [in LF.Logic]
In_example_2 [in LF.Logic]
isAlpha [in LF.ImpParser]
isDigit [in LF.ImpParser]
isLowerAlpha [in LF.ImpParser]
isred [in LF.Basics]
isWhite [in LF.ImpParser]
is_der [in LF.IndProp]
is_even_prime [in LF.Logic]
is_fortytwo [in LF.Auto]
is_three [in LF.Logic]

L

leb [in LF.Basics]
lemma_application_ex [in LF.Logic]
length [in LF.Poly]
length_is_1 [in LF.Poly]
list123 [in LF.Poly]
list123' [in LF.Poly]
list123'' [in LF.Poly]
list123''' [in LF.Poly]
list_of_string [in LF.ImpParser]
loop [in LF.Imp]
lt [in LF.IndProp]
ltb [in LF.Basics]

M

manual_grade_for_baz_num_elts [in LF.Lists]
manual_grade_for_binary [in LF.Basics]
manual_grade_for_binary_commute [in LF.Induction]
manual_grade_for_binary_inverse_a [in LF.Induction]
manual_grade_for_binary_inverse_b [in LF.Induction]
manual_grade_for_binary_inverse_c [in LF.Induction]
manual_grade_for_ceval_step__ceval_inf [in LF.ImpCEvalFun]
manual_grade_for_check_repeats [in LF.IndProp]
manual_grade_for_destruct_induction [in LF.Induction]
manual_grade_for_double_neg_inf [in LF.Logic]
manual_grade_for_filter_challenge [in LF.IndProp]
manual_grade_for_fold_types_different [in LF.Poly]
manual_grade_for_informal_not_PNP [in LF.Logic]
manual_grade_for_informal_proof [in LF.Tactics]
manual_grade_for_mumble_grumble [in LF.Poly]
manual_grade_for_negation_fn_applied_twice [in LF.Basics]
manual_grade_for_NoDup_disjoint_etc [in LF.IndProp]
manual_grade_for_nostutter [in LF.IndProp]
manual_grade_for_no_whiles_terminating [in LF.Imp]
manual_grade_for_pal_pal_app_rev_pal_rev [in LF.IndProp]
manual_grade_for_plus_comm_informal [in LF.Induction]
manual_grade_for_split_combine [in LF.Tactics]
manual_grade_for_XtimesYinZ_spec [in LF.Imp]
many [in LF.ImpParser]
many_helper [in LF.ImpParser]
map [in LF.Poly]
matches_regex [in LF.IndProp]
match_eps [in LF.IndProp]
minustwo [in LF.Basics]
monochrome [in LF.Basics]
MyEquality.four' [in LF.ProofObjects]
MyEquality.singleton [in LF.ProofObjects]
MyIff.iff [in LF.Logic]
mynil [in LF.Poly]
mynil [in LF.Poly]
mynil' [in LF.Poly]
MyNot.not [in LF.Logic]

N

nandb [in LF.Basics]
NatList.add [in LF.Lists]
NatList.alternate [in LF.Lists]
NatList.app [in LF.Lists]
NatList.bag [in LF.Lists]
NatList.count [in LF.Lists]
NatList.countoddmembers [in LF.Lists]
NatList.eqblist [in LF.Lists]
NatList.fst [in LF.Lists]
NatList.fst' [in LF.Lists]
NatList.hd [in LF.Lists]
NatList.hd_error [in LF.Lists]
NatList.length [in LF.Lists]
NatList.manual_grade_for_bag_theorem [in LF.Lists]
NatList.manual_grade_for_rev_injective [in LF.Lists]
NatList.member [in LF.Lists]
NatList.mylist [in LF.Lists]
NatList.mylist1 [in LF.Lists]
NatList.mylist2 [in LF.Lists]
NatList.mylist3 [in LF.Lists]
NatList.nonzeros [in LF.Lists]
NatList.nth_bad [in LF.Lists]
NatList.nth_error [in LF.Lists]
NatList.nth_error' [in LF.Lists]
NatList.oddmembers [in LF.Lists]
NatList.option_elim [in LF.Lists]
NatList.remove_all [in LF.Lists]
NatList.remove_one [in LF.Lists]
NatList.repeat [in LF.Lists]
NatList.rev [in LF.Lists]
NatList.snd [in LF.Lists]
NatList.snd' [in LF.Lists]
NatList.subset [in LF.Lists]
NatList.sum [in LF.Lists]
NatList.swap_pair [in LF.Lists]
NatList.test_add1 [in LF.Lists]
NatList.test_add2 [in LF.Lists]
NatList.test_alternate1 [in LF.Lists]
NatList.test_alternate2 [in LF.Lists]
NatList.test_alternate3 [in LF.Lists]
NatList.test_alternate4 [in LF.Lists]
NatList.test_app1 [in LF.Lists]
NatList.test_app2 [in LF.Lists]
NatList.test_app3 [in LF.Lists]
NatList.test_countoddmembers1 [in LF.Lists]
NatList.test_countoddmembers2 [in LF.Lists]
NatList.test_countoddmembers3 [in LF.Lists]
NatList.test_count1 [in LF.Lists]
NatList.test_count2 [in LF.Lists]
NatList.test_eqblist1 [in LF.Lists]
NatList.test_eqblist2 [in LF.Lists]
NatList.test_eqblist3 [in LF.Lists]
NatList.test_hd₁ [in LF.Lists]
NatList.test_hd₂ [in LF.Lists]
NatList.test_hd_error1 [in LF.Lists]
NatList.test_hd_error2 [in LF.Lists]
NatList.test_hd_error3 [in LF.Lists]
NatList.test_member1 [in LF.Lists]
NatList.test_member2 [in LF.Lists]
NatList.test_nonzeros [in LF.Lists]
NatList.test_nth_error1 [in LF.Lists]
NatList.test_nth_error2 [in LF.Lists]
NatList.test_nth_error3 [in LF.Lists]
NatList.test_oddmembers [in LF.Lists]
NatList.test_remove_all1 [in LF.Lists]
NatList.test_remove_all2 [in LF.Lists]
NatList.test_remove_all3 [in LF.Lists]
NatList.test_remove_all4 [in LF.Lists]
NatList.test_remove_one1 [in LF.Lists]
NatList.test_remove_one2 [in LF.Lists]
NatList.test_remove_one3 [in LF.Lists]
NatList.test_remove_one4 [in LF.Lists]
NatList.test_rev1 [in LF.Lists]
NatList.test_rev2 [in LF.Lists]
NatList.test_subset1 [in LF.Lists]
NatList.test_subset2 [in LF.Lists]
NatList.test_sum1 [in LF.Lists]
NatList.test_tl [in LF.Lists]
NatList.tl [in LF.Lists]
NatPlayground.pred [in LF.Basics]
NatPlayground2.minus [in LF.Basics]
NatPlayground2.mult [in LF.Basics]
NatPlayground2.plus [in LF.Basics]
NatPlayground2.test_mult1 [in LF.Basics]
nat_to_bin [in LF.Induction]
negb [in LF.Basics]
next_weekday [in LF.Basics]
not_even_1001 [in LF.Logic]
not_even_1001' [in LF.Logic]
no_whiles [in LF.Imp]
nth_error [in LF.Poly]

O

oddb [in LF.Basics]
option_map [in LF.Poly]
orb [in LF.Basics]
order [in LF.Rel]

P

parse [in LF.ImpParser]
parseAExp [in LF.ImpParser]
parseAtomicExp [in LF.ImpParser]
parseBExp [in LF.ImpParser]
parseConjunctionExp [in LF.ImpParser]
parseIdentifier [in LF.ImpParser]
parseNumber [in LF.ImpParser]
parsePrimaryExp [in LF.ImpParser]
parseProductExp [in LF.ImpParser]
parser [in LF.ImpParser]
parseSequencedCommand [in LF.ImpParser]
parseSimpleCommand [in LF.ImpParser]
parseSumExp [in LF.ImpParser]
PartialMap.find [in LF.Lists]
PartialMap.update [in LF.Lists]
partial_function [in LF.Rel]
partial_map [in LF.Maps]
partition [in LF.Poly]
peirce [in LF.Logic]
plus' [in LF.Basics]
plus2 [in LF.Imp]
plus3 [in LF.Poly]
plus_fact [in LF.Logic]
preorder [in LF.Rel]
Props.and_comm' [in LF.ProofObjects]
Props.and_comm'_aux [in LF.ProofObjects]
Props.conj_fact [in LF.ProofObjects]
Props.ex_ev_Sn [in LF.ProofObjects]
Props.or_comm [in LF.ProofObjects]
Props.some_nat_is_even [in LF.ProofObjects]
Pumping.napp [in LF.IndProp]
Pumping.pumping_constant [in LF.IndProp]
pup_to_n [in LF.Imp]
pup_to_n [in LF.ImpCEvalFun]
P_m0r [in LF.IndPrinciples]
P_m0r' [in LF.IndPrinciples]

R

reflexive [in LF.Rel]
refl_matches_eps [in LF.IndProp]
regex_match [in LF.IndProp]
reg_exp_ex₁ [in LF.IndProp]
reg_exp_ex₂ [in LF.IndProp]
reg_exp_ex₃ [in LF.IndProp]
reg_exp_ex₄ [in LF.IndProp]
reg_exp_of_list [in LF.IndProp]
relation [in LF.Rel]
repeat [in LF.Poly]
repeat' [in LF.Poly]
repeat'' [in LF.Poly]
repeat''' [in LF.Poly]
rev [in LF.Poly]
rev_append [in LF.Logic]
re_chars [in LF.IndProp]
re_not_empty [in LF.IndProp]
R.fR [in LF.IndProp]
R.manual_grade_for_R_provability [in LF.IndProp]

S

sillyfun [in LF.Tactics]
sillyfun1 [in LF.Tactics]
snd [in LF.Poly]
split [in LF.Tactics]
split [in LF.Poly]
split_combine_statement [in LF.Tactics]
square [in LF.Tactics]
state [in LF.Imp]
string [in LF.IndProp]
string_of_list [in LF.ImpParser]
st₁₂ [in LF.Auto]
st₂₁ [in LF.Auto]
subtract_slowly [in LF.Imp]
subtract_slowly_body [in LF.Imp]
subtract_3_from_5_slowly [in LF.Imp]
symmetric [in LF.Rel]
s_compile [in LF.Imp]
s_compile1 [in LF.Imp]
s_execute [in LF.Imp]
s_execute1 [in LF.Imp]
s_execute2 [in LF.Imp]

T

testParsing [in LF.ImpParser]
test_andb31 [in LF.Basics]
test_andb32 [in LF.Basics]
test_andb33 [in LF.Basics]
test_andb34 [in LF.Basics]
test_anon_fun' [in LF.Poly]
test_ceval [in LF.ImpCEvalFun]
test_countoddmembers'1 [in LF.Poly]
test_countoddmembers'2 [in LF.Poly]
test_countoddmembers'3 [in LF.Poly]
test_der0 [in LF.IndProp]
test_der1 [in LF.IndProp]
test_der2 [in LF.IndProp]
test_der3 [in LF.IndProp]
test_der4 [in LF.IndProp]
test_der5 [in LF.IndProp]
test_der6 [in LF.IndProp]
test_der7 [in LF.IndProp]
test_doit3times [in LF.Poly]
test_doit3times' [in LF.Poly]
test_existsb_1 [in LF.Tactics]
test_existsb_2 [in LF.Tactics]
test_existsb_3 [in LF.Tactics]
test_existsb_4 [in LF.Tactics]
test_factorial1 [in LF.Basics]
test_factorial2 [in LF.Basics]
test_filter1 [in LF.Poly]
test_filter2 [in LF.Poly]
test_filter2' [in LF.Poly]
test_filter_even_gt7_1 [in LF.Poly]
test_filter_even_gt7_2 [in LF.Poly]
test_flat_map1 [in LF.Poly]
test_forallb_1 [in LF.Tactics]
test_forallb_2 [in LF.Tactics]
test_forallb_3 [in LF.Tactics]
test_forallb_4 [in LF.Tactics]
test_hd_error1 [in LF.Poly]
test_hd_error2 [in LF.Poly]
test_leb1 [in LF.Basics]
test_leb2 [in LF.Basics]
test_leb3 [in LF.Basics]
test_leb3' [in LF.Basics]
test_length1 [in LF.Poly]
test_ltb1 [in LF.Basics]
test_ltb2 [in LF.Basics]
test_ltb3 [in LF.Basics]
test_map1 [in LF.Poly]
test_map2 [in LF.Poly]
test_map3 [in LF.Poly]
test_nandb1 [in LF.Basics]
test_nandb2 [in LF.Basics]
test_nandb3 [in LF.Basics]
test_nandb4 [in LF.Basics]
test_next_weekday [in LF.Basics]
test_nostutter_1 [in LF.IndProp]
test_nostutter_2 [in LF.IndProp]
test_nostutter_3 [in LF.IndProp]
test_nostutter_4 [in LF.IndProp]
test_nth_error1 [in LF.Poly]
test_nth_error2 [in LF.Poly]
test_nth_error3 [in LF.Poly]
test_oddb1 [in LF.Basics]
test_oddb2 [in LF.Basics]
test_orb1 [in LF.Basics]
test_orb2 [in LF.Basics]
test_orb3 [in LF.Basics]
test_orb4 [in LF.Basics]
test_orb5 [in LF.Basics]
test_partition1 [in LF.Poly]
test_partition2 [in LF.Poly]
test_plus3 [in LF.Poly]
test_plus3' [in LF.Poly]
test_plus3'' [in LF.Poly]
test_repeat1 [in LF.Poly]
test_repeat2 [in LF.Poly]
test_rev1 [in LF.Poly]
test_rev2 [in LF.Poly]
test_split [in LF.Poly]
token [in LF.ImpParser]
tokenize [in LF.ImpParser]
tokenize_ex₁ [in LF.ImpParser]
tokenize_helper [in LF.ImpParser]
total_map [in LF.Maps]
transitive [in LF.Rel]
trans_eq_example [in LF.Tactics]
trans_eq_example' [in LF.Tactics]
trans_eq_exercise [in LF.Tactics]
tr_rev [in LF.Logic]
t_empty [in LF.Maps]
t_update [in LF.Maps]

U

update [in LF.Maps]
update_example1 [in LF.Maps]
update_example2 [in LF.Maps]
update_example3 [in LF.Maps]
update_example4 [in LF.Maps]

W

W [in LF.Imp]

X

X [in LF.Imp]
XtimesYinZ [in LF.Imp]

Y

Y [in LF.Imp]

Z

Z [in LF.Imp]

---

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

:

_

(1238 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

:

_

(68 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

_

(25 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

_

(19 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

_

(359 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

_

(211 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

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

_

(76 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

_

(479 entries)