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