Global Index

(1106 entries)

Notation Index

(53 entries)

Module Index

(24 entries)

Library Index

(19 entries)

Lemma Index

(329 entries)

Constructor Index

(204 entries)

Axiom Index

(1 entry)

Inductive Index

(73 entries)

Definition Index

(403 entries)

Global Index

A

B

BAnd [constructor, in Imp]
bar [definition, in Tactics]
Basics [library]
baz [inductive, in Lists]
Baz1 [constructor, in Lists]
Baz2 [constructor, in Lists]
bempty [constructor, in IndPrinciples]
BEq [constructor, in Imp]
beq_id [definition, in Maps]
beq_id [definition, in Lists]
beq_idP [lemma, in Maps]
beq_id_false_iff [lemma, in Maps]
beq_id_refl [lemma, in Maps]
beq_id_refl [lemma, in Lists]
beq_id_true [lemma, in Tactics]
beq_id_true_iff [lemma, in Maps]
beq_list [definition, in Logic]
beq_list_true_iff [lemma, in Logic]
beq_nat [definition, in Basics]
beq_natP [lemma, in IndProp]
beq_natP_practice [lemma, in IndProp]
beq_nat_false_iff [lemma, in Logic]
beq_nat_refl [lemma, in Induction]
beq_nat_sym [lemma, in Tactics]
beq_nat_trans [lemma, in Tactics]
beq_nat_true [lemma, in Tactics]
beq_nat_true_iff [lemma, in Logic]
beq_nat_0_l [lemma, in Tactics]
beval [definition, in Imp]
bexp [inductive, in Imp]
bexp1 [definition, in Imp]
BFalse [constructor, in Imp]
Bib [library]
bignumber [definition, in ImpParser]
black [constructor, in Basics]
BLe [constructor, in Imp]
bleaf [constructor, in IndPrinciples]
blt_nat [definition, in Basics]
blue [constructor, in IndPrinciples]
blue [constructor, in Basics]
BNot [constructor, in Imp]
bool [inductive, in Basics]
boollist [inductive, in Poly]
bool_cons [constructor, in Poly]
bool_fn_applied_thrice [lemma, in Tactics]
bool_nil [constructor, in Poly]
BreakImp [module, in Imp]
BreakImp.break_ignore [lemma, in Imp]
BreakImp.CAss [constructor, in Imp]
BreakImp.CBreak [constructor, in Imp]
BreakImp.ceval [inductive, in Imp]
BreakImp.ceval_deterministic [lemma, in Imp]
BreakImp.CIf [constructor, in Imp]
BreakImp.com [inductive, in Imp]
BreakImp.CSeq [constructor, in Imp]
BreakImp.CSkip [constructor, in Imp]
BreakImp.CWhile [constructor, in Imp]
BreakImp.E_Skip [constructor, in Imp]
BreakImp.result [inductive, in Imp]
BreakImp.SBreak [constructor, in Imp]
BreakImp.SContinue [constructor, in Imp]
BreakImp.while_break_true [lemma, in Imp]
BreakImp.while_continue [lemma, in Imp]
BreakImp.while_stops_on_break [lemma, in Imp]
BreakImp.::x_'/'_x_'\\'_x_'/'_x [notation, in Imp]
BreakImp.::x_'::='_x [notation, in Imp]
BreakImp.::x_';;'_x [notation, in Imp]
BreakImp.::'BREAK' [notation, in Imp]
BreakImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Imp]
BreakImp.::'SKIP' [notation, in Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [notation, in Imp]
BTrue [constructor, in Imp]
byntree [inductive, in IndPrinciples]

C

D

day [inductive, in Basics]
de_morgan_not_and_not [definition, in Logic]
digit [constructor, in ImpParser]
dist_exists_or [lemma, in Logic]
dist_not_exists [lemma, in Logic]
doit3times [definition, in Poly]
double [definition, in Induction]
double_injective [lemma, in Tactics]
double_injective_FAILED [lemma, in Tactics]
double_injective_take2 [lemma, in Tactics]
double_injective_take2_FAILED [lemma, in Tactics]
double_neg [lemma, in Logic]
double_negation_elimination [definition, in Logic]
double_plus [lemma, in Induction]

E

F

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

G

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

H

hd_error [definition, in Poly]

I

id [inductive, in Maps]
id [inductive, in Lists]
Id [constructor, in Lists]
Id [constructor, in Maps]
identity_fn_applied_twice [lemma, in Basics]
iff_refl [lemma, in Logic]
iff_reflect [lemma, in IndProp]
iff_sym [lemma, in Logic]
iff_trans [lemma, in Logic]
Imp [library]
ImpCEvalFun [library]
implies_to_or [definition, in Logic]
ImpParser [library]
In [definition, in Logic]
IndPrinciples [library]
IndProp [library]
Induction [library]
injective [definition, in Logic]
inversion_ex₁ [lemma, in Tactics]
inversion_ex₂ [lemma, in Tactics]
inversion_ex₃ [definition, in Tactics]
inversion_ex₄ [lemma, in Tactics]
inversion_ex₅ [lemma, in Tactics]
inversion_ex₆ [definition, in Tactics]
in_app_iff [lemma, in Logic]
In_example_1 [definition, in Logic]
In_example_2 [definition, in Logic]
In_map [lemma, in Logic]
In_map_iff [lemma, in Logic]
in_re_match [lemma, in IndProp]
in_split [lemma, in IndProp]
isAlpha [definition, in ImpParser]
isDigit [definition, in ImpParser]
isLowerAlpha [definition, in ImpParser]
isred [definition, in Basics]
isWhite [definition, in ImpParser]
is_even_prime [definition, in Logic]
is_fortytwo [definition, in Auto]
is_three [definition, in Logic]

L

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

M

many [definition, in ImpParser]
many_helper [definition, in ImpParser]
map [definition, in Poly]
MApp [constructor, in IndProp]
Maps [library]
map_rev [lemma, in Poly]
MChar [constructor, in IndProp]
MEmpty [constructor, in IndProp]
minustwo [definition, in Basics]
minus_diag [lemma, in Induction]
monday [constructor, in Basics]
monochrome [definition, in Basics]
MStarApp [constructor, in IndProp]
MStar' [lemma, in IndProp]
MStar'' [lemma, in IndProp]
MStar0 [constructor, in IndProp]
MStar1 [lemma, in IndProp]
mult_assoc [lemma, in Induction]
mult_comm [lemma, in Induction]
mult_eq_0 [lemma, in Logic]
mult_plus_distr_r [lemma, in Induction]
mult_S_1 [lemma, in Basics]
mult_0 [lemma, in Logic]
mult_0_l [lemma, in Basics]
mult_0_plus [lemma, in Basics]
mult_0_plus' [lemma, in Induction]
mult_0_r [lemma, in Induction]
mult_0_r' [lemma, in IndPrinciples]
mult_0_r'' [lemma, in IndPrinciples]
mult_0_3 [lemma, in Logic]
mult_1_l [lemma, in Induction]
MumbleGrumble [module, in Poly]
MumbleGrumble.a [constructor, in Poly]
MumbleGrumble.b [constructor, in Poly]
MumbleGrumble.c [constructor, in Poly]
MumbleGrumble.d [constructor, in Poly]
MumbleGrumble.e [constructor, in Poly]
MumbleGrumble.grumble [inductive, in Poly]
MumbleGrumble.mumble [inductive, in Poly]
MUnionL [constructor, in IndProp]
MUnionR [constructor, in IndProp]
MUnion' [lemma, in IndProp]
MyEquality [module, in ProofObjects]
MyEquality.eq [inductive, in ProofObjects]
MyEquality.eq_refl [constructor, in ProofObjects]
MyEquality.four [lemma, in ProofObjects]
MyEquality.four' [definition, in ProofObjects]
MyEquality.leibniz_equality [lemma, in ProofObjects]
MyEquality.singleton [definition, in ProofObjects]
MyEquality.:type_scope:x_'='_x [notation, in ProofObjects]
MyIff [module, in Logic]
MyIff.iff [definition, in Logic]
MyIff.:type_scope:x_'<->'_x [notation, in Logic]
mynil [definition, in Poly]
mynil [definition, in Poly]
mynil' [definition, in Poly]
MyNot [module, in Logic]
MyNot.not [definition, in Logic]
MyNot.:type_scope:'~'_x [notation, in Logic]

N

O

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

P

R

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

S

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

T

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

U

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

W

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

X

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

Y

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

Z

Z [definition, in Imp]
zero_nbeq_plus_1 [lemma, in Basics]
zero_nbeq_S [lemma, in Induction]
zero_not_one [lemma, in Logic]
zero_not_one' [lemma, in Logic]
zero_or_succ [lemma, in Logic]

:

:nat_scope:x_'*'_x [notation, in Basics]
:nat_scope:x_'*'_x [notation, in Basics]
:nat_scope:x_'+'_x [notation, in Basics]
:nat_scope:x_'+'_x [notation, in Basics]
:nat_scope:x_'-'_x [notation, in Basics]
:nat_scope:x_'<=?'_x [notation, in ImpParser]
:type_scope:x_'*'_x [notation, in Poly]
::x_'&&'_x [notation, in Basics]
::x_'++'_x [notation, in Poly]
::x_'/'_x_'\\'_x [notation, in Imp]
::x_'::'_x [notation, in Poly]
::x_'::='_x [notation, in Imp]
::x_';;'_x [notation, in Imp]
::x_'<'_x [notation, in IndProp]
::x_'<='_x [notation, in IndPrinciples]
::x_'=~'_x [notation, in IndProp]
::x_'||'_x [notation, in Basics]
::'DO'_'('_x_','_x_')'_'<--'_x_';'_x_'OR'_x [notation, in ImpParser]
::'DO'_'('_x_','_x_')'_'<=='_x_';'_x [notation, in ImpParser]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Imp]
::'LETOPT'_x_'<=='_x_'IN'_x [notation, in ImpCEvalFun]
::'SKIP' [notation, in Imp]
::'WHILE'_x_'DO'_x_'END' [notation, in Imp]
::'('_x_','_x_')' [notation, in Poly]
::'['_x_';'_'..'_';'_x_']' [notation, in Poly]
::'['_']' [notation, in Poly]

Notation Index

A

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

B

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

M

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

N

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

P

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

R

Repeat.::x_'/'_x_'\\'_x [in Auto]
Repeat.::x_'::='_x [in Auto]
Repeat.::x_';'_x [in Auto]
Repeat.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Auto]
Repeat.::'REPEAT'_x_'UNTIL'_x_'END' [in Auto]
Repeat.::'SKIP' [in Auto]
Repeat.::'WHILE'_x_'DO'_x_'END' [in Auto]

:

:nat_scope:x_'*'_x [in Basics]
:nat_scope:x_'*'_x [in Basics]
:nat_scope:x_'+'_x [in Basics]
:nat_scope:x_'+'_x [in Basics]
:nat_scope:x_'-'_x [in Basics]
:nat_scope:x_'<=?'_x [in ImpParser]
:type_scope:x_'*'_x [in Poly]
::x_'&&'_x [in Basics]
::x_'++'_x [in Poly]
::x_'/'_x_'\\'_x [in Imp]
::x_'::'_x [in Poly]
::x_'::='_x [in Imp]
::x_';;'_x [in Imp]
::x_'<'_x [in IndProp]
::x_'<='_x [in IndPrinciples]
::x_'=~'_x [in IndProp]
::x_'||'_x [in Basics]
::'DO'_'('_x_','_x_')'_'<--'_x_';'_x_'OR'_x [in ImpParser]
::'DO'_'('_x_','_x_')'_'<=='_x_';'_x [in ImpParser]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Imp]
::'LETOPT'_x_'<=='_x_'IN'_x [in ImpCEvalFun]
::'SKIP' [in Imp]
::'WHILE'_x_'DO'_x_'END' [in Imp]
::'('_x_','_x_')' [in Poly]
::'['_x_';'_'..'_';'_x_']' [in Poly]
::'['_']' [in Poly]

Module Index

A

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

B

BreakImp [in Imp]

E

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

F

FirstTry [in IndProp]

M

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

N

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

P

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

R

R [in IndProp]
Repeat [in 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 Imp]
AExp.aeval_iff_aevalR' [in Imp]
AExp.beval_iff_bevalR [in Imp]
AExp.foo [in Imp]
AExp.foo' [in Imp]
AExp.In10 [in Imp]
AExp.In10' [in Imp]
AExp.optimize_0plus_b_sound [in Imp]
AExp.optimize_0plus_sound [in Imp]
AExp.optimize_0plus_sound' [in Imp]
AExp.optimize_0plus_sound'' [in Imp]
AExp.silly1 [in Imp]
AExp.silly2 [in Imp]
all3_spec [in Induction]
All_In [in Logic]
andb3_exchange [in Basics]
andb_commutative [in Basics]
andb_commutative' [in Basics]
andb_commutative'' [in Basics]
andb_eq_orb [in Basics]
andb_false_r [in Induction]
andb_true_elim2 [in Basics]
andb_true_iff [in Logic]
and_assoc [in Logic]
and_commut [in Logic]
and_example2 [in Logic]
and_example2' [in Logic]
and_example2'' [in Logic]
and_example3 [in Logic]
and_intro [in Logic]
apply_empty [in Maps]
apply_iff_example [in Logic]
app_assoc [in Poly]
app_length [in Poly]
app_nil_r [in Poly]

B

beq_idP [in Maps]
beq_id_false_iff [in Maps]
beq_id_refl [in Maps]
beq_id_refl [in Lists]
beq_id_true [in Tactics]
beq_id_true_iff [in Maps]
beq_list_true_iff [in Logic]
beq_natP [in IndProp]
beq_natP_practice [in IndProp]
beq_nat_false_iff [in Logic]
beq_nat_refl [in Induction]
beq_nat_sym [in Tactics]
beq_nat_trans [in Tactics]
beq_nat_true [in Tactics]
beq_nat_true_iff [in Logic]
beq_nat_0_l [in Tactics]
bool_fn_applied_thrice [in Tactics]
BreakImp.break_ignore [in Imp]
BreakImp.ceval_deterministic [in Imp]
BreakImp.while_break_true [in Imp]
BreakImp.while_continue [in Imp]
BreakImp.while_stops_on_break [in Imp]

C

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

D

dist_exists_or [in Logic]
dist_not_exists [in Logic]
double_injective [in Tactics]
double_injective_FAILED [in Tactics]
double_injective_take2 [in Tactics]
double_injective_take2_FAILED [in Tactics]
double_neg [in Logic]
double_plus [in Induction]

E

empty_is_empty [in IndProp]
evenb_double [in Logic]
evenb_double_conv [in Logic]
evenb_S [in Induction]
even5_nonsense [in IndProp]
even_bool_prop [in Logic]
evSS_ev [in IndProp]
evSS_ev [in IndProp]
ev'_ev [in IndProp]
ev_double [in IndProp]
ev_even [in IndProp]
ev_even_firsttry [in IndProp]
ev_even_iff [in IndProp]
ev_ev' [in IndPrinciples]
ev_ev__ev [in IndProp]
ev_minus2 [in IndProp]
ev_minus2' [in IndProp]
ev_plus4 [in ProofObjects]
ev_plus4 [in IndProp]
ev_plus_plus [in IndProp]
ev_sum [in IndProp]
ev_4 [in ProofObjects]
ev_4 [in IndProp]
ev_4' [in ProofObjects]
ev_4' [in IndProp]
ev_4'' [in ProofObjects]
ev_8 [in ProofObjects]
excluded_middle_irrefutable [in Logic]
Exercises.curry_uncurry [in Poly]
Exercises.fold_length_correct [in Poly]
Exercises.uncurry_curry [in Poly]
exists_example_2 [in Logic]
ex_falso_quodlibet [in Logic]

F

false_beq_id [in Maps]
filter_exercise [in Tactics]
filter_not_empty_In [in IndProp]
filter_not_empty_In' [in IndProp]
forallb_true_iff [in Logic]
four_is_even [in Logic]
f_equal [in Tactics]

I

identity_fn_applied_twice [in Basics]
iff_refl [in Logic]
iff_reflect [in IndProp]
iff_sym [in Logic]
iff_trans [in Logic]
inversion_ex₁ [in Tactics]
inversion_ex₂ [in Tactics]
inversion_ex₄ [in Tactics]
inversion_ex₅ [in Tactics]
in_app_iff [in Logic]
In_map [in Logic]
In_map_iff [in Logic]
in_re_match [in IndProp]
in_split [in IndProp]

L

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

M

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

N

O

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

P

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

R

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

S

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

T

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

U

update_eq [in Maps]
update_neq [in Maps]
update_permute [in Maps]
update_same [in Maps]
update_shadow [in Maps]

Z

zero_nbeq_plus_1 [in Basics]
zero_nbeq_S [in Induction]
zero_not_one [in Logic]
zero_not_one' [in Logic]
zero_or_succ [in Logic]

Constructor Index

A

B

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

C

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

D

digit [in ImpParser]

E

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

F

false [in Basics]
FirstTry.ReflectF [in IndProp]
FirstTry.ReflectT [in IndProp]
friday [in Basics]

G

green [in Basics]
green [in IndPrinciples]

I

Id [in Lists]
Id [in Maps]

L

leaf [in IndPrinciples]
le_n [in IndPrinciples]
le_S [in IndPrinciples]

M

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

N

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

O

other [in ImpParser]

P

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

R

S

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

T

thursday [in Basics]
true [in Basics]
tuesday [in Basics]

U

Union [in IndProp]

W

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

Y

yes [in IndPrinciples]

Axiom Index

F

functional_extensionality [in Logic]

Inductive Index

A

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

B

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

C

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

D

day [in Basics]

E

ev [in IndProp]
ev' [in IndProp]
exp_match [in IndProp]
ExSet [in IndPrinciples]

F

FirstTry.reflect [in IndProp]
foo' [in IndPrinciples]

I

id [in Maps]
id [in Lists]

L

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

M

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

N

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

O

option [in Poly]
optionE [in ImpParser]

P

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

R

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

S

sinstr [in Imp]
square_of [in IndProp]

T

tree [in IndPrinciples]

W

wrong_ev [in IndProp]

Y

yesno [in IndPrinciples]

Definition Index

A

B

bar [in Tactics]
beq_id [in Maps]
beq_id [in Lists]
beq_list [in Logic]
beq_nat [in Basics]
beval [in Imp]
bexp1 [in Imp]
bignumber [in ImpParser]
blt_nat [in Basics]

C

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

D

de_morgan_not_and_not [in Logic]
doit3times [in Poly]
double [in Induction]
double_negation_elimination [in Logic]

E

F

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

H

hd_error [in Poly]

I

implies_to_or [in Logic]
In [in Logic]
injective [in Logic]
inversion_ex₃ [in Tactics]
inversion_ex₆ [in Tactics]
In_example_1 [in Logic]
In_example_2 [in Logic]
isAlpha [in ImpParser]
isDigit [in ImpParser]
isLowerAlpha [in ImpParser]
isred [in Basics]
isWhite [in ImpParser]
is_even_prime [in Logic]
is_fortytwo [in Auto]
is_three [in Logic]

L

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

M

many [in ImpParser]
many_helper [in ImpParser]
map [in Poly]
minustwo [in Basics]
monochrome [in Basics]
MyEquality.four' [in ProofObjects]
MyEquality.singleton [in ProofObjects]
MyIff.iff [in Logic]
mynil [in Poly]
mynil [in Poly]
mynil' [in Poly]
MyNot.not [in Logic]

N

O

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

P

R

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

S

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

T

testParsing [in ImpParser]
test_andb31 [in Basics]
test_andb32 [in Basics]
test_andb33 [in Basics]
test_andb34 [in Basics]
test_anon_fun' [in Poly]
test_blt_nat1 [in Basics]
test_blt_nat2 [in Basics]
test_blt_nat3 [in Basics]
test_ceval [in ImpCEvalFun]
test_countoddmembers'1 [in Poly]
test_countoddmembers'2 [in Poly]
test_countoddmembers'3 [in Poly]
test_doit3times [in Poly]
test_doit3times' [in Poly]
test_factorial1 [in Basics]
test_factorial2 [in Basics]
test_filter1 [in Poly]
test_filter2 [in Poly]
test_filter2' [in Poly]
test_filter_even_gt7_1 [in Poly]
test_filter_even_gt7_2 [in Poly]
test_flat_map1 [in Poly]
test_hd_error1 [in Poly]
test_hd_error2 [in Poly]
test_leb1 [in Basics]
test_leb2 [in Basics]
test_leb3 [in Basics]
test_length1 [in Poly]
test_map1 [in Poly]
test_map2 [in Poly]
test_map3 [in Poly]
test_nandb1 [in Basics]
test_nandb2 [in Basics]
test_nandb3 [in Basics]
test_nandb4 [in Basics]
test_next_weekday [in Basics]
test_nostutter_1 [in IndProp]
test_nostutter_2 [in IndProp]
test_nostutter_3 [in IndProp]
test_nostutter_4 [in IndProp]
test_nth_error1 [in Poly]
test_nth_error2 [in Poly]
test_nth_error3 [in Poly]
test_oddb1 [in Basics]
test_oddb2 [in Basics]
test_orb1 [in Basics]
test_orb2 [in Basics]
test_orb3 [in Basics]
test_orb4 [in Basics]
test_orb5 [in Basics]
test_partition1 [in Poly]
test_partition2 [in Poly]
test_plus3 [in Poly]
test_plus3' [in Poly]
test_plus3'' [in Poly]
test_repeat1 [in Poly]
test_repeat2 [in Poly]
test_rev1 [in Poly]
test_rev2 [in Poly]
test_split [in Poly]
token [in ImpParser]
tokenize [in ImpParser]
tokenize_ex₁ [in ImpParser]
tokenize_helper [in ImpParser]
total_map [in Maps]
transitive [in Rel]
trans_eq_example [in Tactics]
trans_eq_example' [in Tactics]
trans_eq_exercise [in Tactics]
tr_rev [in Logic]
t_empty [in Maps]
t_update [in Maps]

U

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

W

W [in Imp]

X

X [in Imp]
XtimesYinZ [in Imp]

Y

Y [in Imp]

Z

Z [in Imp]

Global Index

(1106 entries)

Notation Index

(53 entries)

Module Index

(24 entries)

Library Index

(19 entries)

Lemma Index

(329 entries)

Constructor Index

(204 entries)

Axiom Index

(1 entry)

Inductive Index

(73 entries)

Definition Index

(403 entries)