week1: tweaks

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/week1.mdwn b/week1.mdwn
index cacb73f..af079ed 100644 (file)
--- a/week1.mdwn
+++ b/week1.mdwn
@@ -59,6 +59,8 @@ We'll tend to write <code>(&lambda;a M)</code> as just `(\a M)`, so we don't hav
 
 Some authors reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
 
 
 Some authors reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
 

+Samples of expressions
+

 The *lambda* calculus has an associated proof theory. For now, we can regard the proof theory as having just one rule, called the rule of **beta-reduction** or "beta-contraction". Suppose you have some expression of the form:
 
        ((\a M) N)
 The *lambda* calculus has an associated proof theory. For now, we can regard the proof theory as having just one rule, called the rule of **beta-reduction** or "beta-contraction". Suppose you have some expression of the form:
 
        ((\a M) N)