-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term contains more than one
-redex, we have to choose which one to reduce, and this choice can make
-a difference. For instance, in the term `((\x.I)(ωω))`, if we reduce
-the leftmost redex first, the term reduces to the normal form `I` in
-one step. But if we reduce the left most redex instead (namely,
-`(ωω)`), we do not arrive at a normal form, and are in danger of
-entering an infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding of evaluation order by
-writing a program that experiments with different evaluation order
-strategies.
+We've discussed [[evaluation order|topics/week3_evaluation_order]]
+before, primarily in connection with the untyped lambda calculus.
+Whenever a term contains more than one redex, we have to choose which
+one to reduce, and this choice can make a difference. For instance,
+recall that
+
+ Ω == ωω == (\x.xx)(\x.xx), so
+
+ ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
+ * *
+
+There are two redexes in this term; we've marked the operative lambdas
+with a star. If we reduce the leftmost redex first, the term reduces
+to the normal form `I` in one step. But if we reduce the left most
+redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
+danger of entering an infinite loop.
+
+Thanks to the recent introduction of sum types (disjoint union), we
+are now in a position to gain a deeper understanding of evaluation
+order by reasoning explicitly about evaluation by writing a program
+that evaluates terms.