-
Notifications
You must be signed in to change notification settings - Fork 1
/
Review1.v
121 lines (54 loc) · 2.52 KB
/
Review1.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
(** * Review1: Review Session for First Midterm *)
Require Export MoreInd.
(* ###################################################################### *)
(** * General Notes *)
(** *** Standard vs. Advanced Exams *)
(** - Unlike the homework assignments, we will make up two completely
separate versions of the exam -- a "standard exam" and an
"advanced exam." They will share some problems, but there will
be problems on each that are not on the other.
You can choose to take whichever one you want at the beginning
of the exam period.
*)
(** *** Grading *)
(** - Meaning of grades:
- A = mastery of all or almost all of the material
- B = good understanding of most of the material, perhaps with
a few gaps
- C = some understanding of most of the material, with
substantial gaps
- D = major gaps
- F = didn't show up / try
- There is no pre-determined curve. We'd be perfectly delighted
to give everyone an A (for the exam, and for the course).
- Except: A+ grades will be given only for completing the
advanced track.
- Standard and advanced exams will be graded relative to different
expectations (i.e., "the material" is different)
*)
(** *** Hints *)
(**
- On each version of the exam, will be at least one problem taken
more or less verbatim from a homework assignment.
- On the advanced version, there will be an informal proof.
*)
(* ###################################################################### *)
(** * Expressions and Their Types *)
(** Thinking about well-typed expressions and their types is a great
way of reviewing many aspects of how Coq works...
*)
(** (Discussion of Coq's view of the universe...) #<br><br><br><br><br><br><br># *)
(* ###################################################################### *)
(** * Inductive Definitions *)
(* ###################################################################### *)
(** * Tactics *)
(* ###################################################################### *)
(** * Proof Objects*)
(* ###################################################################### *)
(** * Functional Programming *)
(* ###################################################################### *)
(** * Judging Propositions *)
(* ###################################################################### *)
(** * More Type Checking*)
(** Good luck on the exam! *)
(* $Date: 2013-09-26 14:40:26 -0400 (Thu, 26 Sep 2013) $ *)