Global Index

A

a [lemma, in HW5]
add [axiom, in HW7]
add [definition, in HW7]
add [definition, in HW7]
alist [definition, in HW6]
and_associates [lemma, in HW1]
App [constructor, in HW5]
App [constructor, in HW5]
append [definition, in HW2]
append [definition, in HW0]
append_associative [lemma, in HW2]
append_associative [lemma, in HW0]
Arrow [constructor, in HW5]
Arrow [constructor, in HW5]
asgn [definition, in HW6]

bool_and [definition, in HW2]
bool_eq [definition, in HW2]
bool_eq_dec [definition, in HW6]
bool_not [definition, in HW2]
bool_or [definition, in HW2]
bool_xor [definition, in HW2]
boundedSat [definition, in HW6]
boundedSatSimple [definition, in HW6]

chooseSplit [definition, in HW6]
clause [definition, in HW6]
coalesce1 [lemma, in HW1]
coalesce2 [lemma, in HW1]
cons [constructor, in HW2]
Cons [constructor, in HW7]
cons [constructor, in HW0]
Const [constructor, in HW2]
Const [constructor, in HW5]
Const [constructor, in HW5]
constant_fold [definition, in HW2]
constant_folded [definition, in HW2]
constant_fold_simplifies [lemma, in HW2]
constant_fold_sound [lemma, in HW2]
context [definition, in HW5]
context [definition, in HW5]
contradiction_P [lemma, in HW1]
contradictory_assignment [lemma, in HW6]
contrapositive [lemma, in HW1]
cut_out_the_middle_man [lemma, in HW1]

dict [axiom, in HW7]
dict [definition, in HW7]
dict [definition, in HW7]
DICTIONARY [module, in HW7]
DICTIONARY_PARAM [module, in HW7]
dict' [inductive, in HW7]
domain [axiom, in HW7]
domain [definition, in HW7]
domain [definition, in HW7]
domain [axiom, in HW7]
domain [definition, in HW7]
domain [definition, in HW7]
domain_eq_dec [axiom, in HW7]

empty [definition, in HW7]
empty [axiom, in HW7]
empty [definition, in HW7]
eq_transitive [definition, in HW4]
eval [definition, in HW2]
example [definition, in HW4]
exp [inductive, in HW2]

findUnitClause [definition, in HW6]
formula [definition, in HW6]
Fst [constructor, in HW5]
FuncDictionary [module, in HW7]

hasType [inductive, in HW5]
hasType [inductive, in HW5]
hasType_wellFormed [lemma, in HW5]
hasType_wellFormed [lemma, in HW5]
Him [constructor, in HW5]
HT_App [constructor, in HW5]
HT_App [constructor, in HW5]
HT_Const [constructor, in HW5]
HT_Const [constructor, in HW5]
HT_Fst [constructor, in HW5]
HT_Lam [constructor, in HW5]
HT_Lam [constructor, in HW5]
HT_Pair [constructor, in HW5]
HT_Snd [constructor, in HW5]
HT_Var [constructor, in HW5]
HT_Var [constructor, in HW5]
HW0 [library]
HW1 [library]
HW2 [library]
HW3 [library]
HW4 [library]
HW5 [library]
HW6 [library]
HW7 [library]

indeed [lemma, in HW1]
insert [definition, in HW2]
insert_increases [lemma, in HW2]
insert_ordered [lemma, in HW2]
interp_alist [definition, in HW6]
isNil [definition, in HW6]

Lam [constructor, in HW5]
Lam [constructor, in HW5]
last [axiom, in HW3]
lasts_agree1 [lemma, in HW3]
lasts_agree2 [lemma, in HW3]
last_f [axiom, in HW3]
Leaf [constructor, in HW2]
Leaf_neq_Node [lemma, in HW2]
list [inductive, in HW0]
list [inductive, in HW2]
ListDictionary [module, in HW7]
lit [definition, in HW6]
lookup [definition, in HW7]
lookup [inductive, in HW5]
lookup [inductive, in HW5]
lookup [definition, in HW7]
lookup [axiom, in HW7]
lookup' [definition, in HW7]
Lookup_O [constructor, in HW5]
Lookup_O [constructor, in HW5]
Lookup_S [constructor, in HW5]
Lookup_S [constructor, in HW5]

make_up_your_mind [lemma, in HW1]
Me [constructor, in HW5]
mp3 [lemma, in HW5]
my_list_ind [axiom, in HW4]
my_nat_ind [axiom, in HW4]

nasty [lemma, in HW1]
Nat [constructor, in HW5]
Nat [constructor, in HW5]
negate [definition, in HW6]
nil [constructor, in HW0]
Nil [constructor, in HW7]
nil [constructor, in HW2]
nobody [lemma, in HW1]
Node [constructor, in HW2]
Node_inj [lemma, in HW2]
not_and_or_not [lemma, in HW2]
no_identities [definition, in HW2]

ofcourse [lemma, in HW1]
one_or_the_other [lemma, in HW1]
ordered [definition, in HW2]
ordered' [definition, in HW2]
or_associates [lemma, in HW1]
or_commutes [lemma, in HW1]

Pair [constructor, in HW5]
permutation [axiom, in HW3]
permutation_reflexive [lemma, in HW3]
permutation_symmetric [lemma, in HW3]
permutation_transitive [lemma, in HW3]
PLC [module, in HW5]
Plus [constructor, in HW2]
Prod [constructor, in HW5]

reverse [definition, in HW2]
reverse' [definition, in HW2]
reverse'_correct [lemma, in HW2]
reverse'_helper [definition, in HW2]
reverse_congruence [lemma, in HW1]

satClause [definition, in HW6]
satFormula [definition, in HW6]
satLit [definition, in HW6]
satLit_contra [lemma, in HW6]
satLit_dec [lemma, in HW6]
satLit_idem_clause [lemma, in HW6]
satLit_idem_formula [lemma, in HW6]
satLit_idem_lit [lemma, in HW6]
satLit_upd_eq [lemma, in HW6]
satLit_upd_neq [lemma, in HW6]
satLit_upd_neq2 [lemma, in HW6]
setClause [definition, in HW6]
setClauseSimple [definition, in HW6]
setFormula [definition, in HW6]
setFormulaSimple [definition, in HW6]
simplify_identities [definition, in HW2]
simplify_identities_simplifies [lemma, in HW2]
simplify_identities_sound [lemma, in HW2]
size [definition, in HW2]
small_world [lemma, in HW1]
Snd [constructor, in HW5]
somebody [inductive, in HW5]
something_fishy [lemma, in HW1]
STLC [module, in HW5]
swap_quantifiers [lemma, in HW1]
swap_quantifiers [definition, in HW4]
swap_quantifiers2 [definition, in HW4]

term [inductive, in HW5]
term [inductive, in HW5]
term1 [definition, in HW4]
term2 [definition, in HW4]
term3 [definition, in HW4]
term4 [definition, in HW4]
testIt [lemma, in HW5]
Times [constructor, in HW2]
transpose [axiom, in HW3]
tree [inductive, in HW2]
truth [lemma, in HW1]
type [inductive, in HW5]
type [inductive, in HW5]

uniqueness [lemma, in HW5]
uniqueness [lemma, in HW5]
unitClauseTrue [lemma, in HW6]
unitPropagate [definition, in HW6]
unitPropagateSimple [definition, in HW6]
upd [definition, in HW6]

Var [constructor, in HW5]
var [definition, in HW6]
Var [constructor, in HW5]
Var [constructor, in HW2]
var [definition, in HW2]

wellFormed [inductive, in HW5]
wellFormed [inductive, in HW5]
WF_App [constructor, in HW5]
WF_App [constructor, in HW5]
WF_Const [constructor, in HW5]
WF_Const [constructor, in HW5]
WF_Fst [constructor, in HW5]
WF_Lam [constructor, in HW5]
WF_Lam [constructor, in HW5]
WF_Pair [constructor, in HW5]
WF_Snd [constructor, in HW5]
WF_Var [constructor, in HW5]
WF_Var [constructor, in HW5]