TSPL survey

courses/tspl/2019/survey

@@ -0,0 +1,106 @@
+
+How likely is it that you would recommend your class to another student?
+------------------------------------------------------------------------
+
+DETRACTORS (0-6)		0
+PASSIVES (7-8)			6
+PROMOTERS (9-10)		5
+TOTAL				11
+
+
+Was the speed with which your instructor presented the course material
+too fast, too slow, or about right?
+----------------------------------------------------------------------
+
+Much too fast		0
+Too fast		3
+The right amount	8
+Too slow		0
+Much too slow		0
+TOTAL			11
+
+
+What did you like about the class?
+----------------------------------
+
+Very entertaining lectures, stimulating content and the workload feels
+just right for a 10 credit module. One of my favourite classes I've
+taken in my university career
+
+Agda is extremely interesting and help with understanding the material
+presented in the lectures. The assignments are challenging and fun.
+
+too many assignments
+
+Engaging lecturer, useful tutorials, well administered (everything on
+GitHub + GitHub pages + improvements via pull requests are
+encouraged).
+
+Lots of support in tutorials
+
+The professor is so passionate.
+
+Professor: humorous language, passionate teaching.
+
+Engaging lecturer, small class, most hands-on tuition I've received
+out of any class at this university with both the lecturer and the TAs
+giving you 3 hrs of their time each week just to help you out with the
+exercises. Instant feedback on your thought process, presented in a
+helpful and friendly way.
+
+Interesting content, agda is a lot of fun to use
+
+Extremely capable lecturer, and the tutorials are both enjoyable to
+complete and it’s great how classmates can help each other out because
+solutions need not be secretive
+
+Enthusiasm of lecturer, large amount of contact hours.
+
+
+
+What would you change?
+----------------------
+
+The logical foundations part of the course felt like it dragged on for
+a very long time. I think this was just because I knew that we'd get
+to the exciting part later and that it was being put off by the LF
+part, and that I had already taken modules vaguely in this area and
+was quite confident with that content However, during the actual PLF
+part I feel like it's suddenly got much harder and we've almost rushed
+through things. The difficulty feels a little imbalanced, but that's
+ok as you would generally expect a course to get harder as time goes
+on.
+
+More structure around the project/essay, I’m not sure how to approach
+it. More type theory. The course demonstrates the power of dependent
+types in Agda, it would be nice to look in to the theory behind
+them. Also sorts, I have seen it in error messages but not quite sure
+what they are.
+
+Lecture recordings, for later recap Not about this course, but more
+courses need to use github
+
+Go slower on part 2
+
+nothing
+
+Nothing
+
+As soon as part 2 started I found it much harder to absorb the
+material covered in the lectures. I suspect this is due to the
+increasingly technical material making it harder to give proofs live,
+leading to too much of just reading the course textbook out loud
+(though this was still helpful, as reading the technical bits is in
+itself a sizeable challenge at times). If possible I think it could be
+helpful to do some more live proofs in part 2.
+
+The pace of part 1 feels right. Part 2 feels very rushed, and I don't
+think enough time has been spent on any area of it for me to really
+follow what's going on. I would suggest giving more lectures in part
+2, ideally by extending the total number of lectures.
+
+Make it more credits/double term - just more would be great
+
+Part 2 of the course covers too short a time period. I think the
+course should either span the whole 10 weeks of the semester, or Part
+1 should be taught quicker to make time for Part 2

src/plfa/part2/Untyped.lagda.md

@@ -346,15 +346,6 @@ The evidence that a term is in normal form is almost identical to
 the term itself, decorated with some additional primes to indicate
 neutral terms, and using `#′` in place of `#`
 
-We will also need to characterise terms that are applications:
-```
-data Application : ∀ {Γ A} → Γ ⊢ A → Set where
-
-  ap : ∀ {Γ} {L M : Γ ⊢ ★}
-      -------------------
-    → Application (L · M)
-```
-
 
 ## Reduction step