Add Scrutinee binder removal.

[matthijs/master-project/report.git] / Chapters / Prototype.tex

diff --git a/Chapters/Prototype.tex b/Chapters/Prototype.tex
index 7d99104629c0ecbe92d76829b30fa0637dc69874..101594bf2a9b4aaacbd210c1242fd968ed0f2fa7 100644 (file)
--- a/Chapters/Prototype.tex
+++ b/Chapters/Prototype.tex
@@ -516,12 +516,12 @@
       
       A case expression evaluates its scrutinee, which should have an
       algebraic datatype, into weak head normal form (\small{WHNF}) and
-      (optionally) binds it to \lam{bndr}. Every alternative lists a
-      single constructor (\lam{C0 ... Cn}). Based on the actual
-      constructor of the scrutinee, the corresponding alternative is
-      chosen. The binders in the chosen alternative (\lam{bndr0,0 ....
-      bndr0,m} are bound to the actual arguments to the constructor in
-      the scrutinee.
+      (optionally) binds it to \lam{bndr}. If bndr is wild, \refdef{wild
+      binders} it is left out.  Every alternative lists a single constructor
+      (\lam{C0 ... Cn}). Based on the actual constructor of the scrutinee, the
+      corresponding alternative is chosen. The binders in the chosen
+      alternative (\lam{bndr0,0 ....  bndr0,m} are bound to the actual
+      arguments to the constructor in the scrutinee.
 
       This is best illustrated with an example. Assume
       there is an algebraic datatype declared as follows\footnote{This