projects
/
lambda.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
week4 tweaking
[lambda.git]
/
week4.mdwn
diff --git
a/week4.mdwn
b/week4.mdwn
index
5238b26
..
78e2d37
100644
(file)
--- a/
week4.mdwn
+++ b/
week4.mdwn
@@
-69,9
+69,9
@@
succ X
≡ (\n s z. s (n s z)) X
~~> \s z. s (X s z)
<~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
≡ (\n s z. s (n s z)) X
~~> \s z. s (X s z)
<~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-
~~> \s z. s ([succ (\s z. s (X s z))] s z
)
-~~> \s z. s (
[\s z. s ([succ (\s z. s (X s z))] s z)]
s z)
-~~> \s z. s (s (
succ (\s z. s (X s z))
))
+
≡ (\n s z. s (n s z)) (\s z. s (X s z)
)
+~~> \s z. s (
(\s z. s (X s z))
s z)
+~~> \s z. s (s (
X s z
))
</code></pre>
So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
</code></pre>
So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,