week1: fix markup processing?
authorJim Pryor <profjim@jimpryor.net>
Thu, 16 Sep 2010 02:45:15 +0000 (22:45 -0400)
committerJim Pryor <profjim@jimpryor.net>
Thu, 16 Sep 2010 02:45:15 +0000 (22:45 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
test2.mdwn [new file with mode: 0644]
week1.mdwn

diff --git a/test2.mdwn b/test2.mdwn
new file mode 100644 (file)
index 0000000..be55fef
--- /dev/null
@@ -0,0 +1,17 @@
+
+Some authors reserve the term "term" for just variables and abstracts. We'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
+
+Examples of expressions:
+
+       x
+       (y x)
+       (x x)
+       (\x y)
+       (\x x)
+       (\x (\y x))
+       (x (\x x))
+       ((\x (x x)) (\x (x x)))
+
+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:
index b5a67fa..36ebdfc 100644 (file)
@@ -59,9 +59,16 @@ 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'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'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
 
-Examples *of* expressions:
+Examples of expressions:
 
        x
 
        x
+       (y x)
+       (x x)
+       (\x y)
+       (\x x)
+       (\x (\y x))
+       (x (\x x))
+       ((\x (x x)) (\x (x x)))
 
 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
 
 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