# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1224683017 14400
# Node ID 464db50b210a99dd403d1574c44711dd3bc9968d
# Parent  fd52e2a7ffc3d6d625efc494348a120074d82955
Clarify intent to use hlist

diff -r fd52e2a7ffc3 -r 464db50b210a src/DataStruct.v
--- a/src/DataStruct.v	Wed Oct 22 07:50:47 2008 -0400
+++ b/src/DataStruct.v	Wed Oct 22 09:43:37 2008 -0400
@@ -833,7 +833,7 @@
 
   Repeat this process so that you implement each definition for each of the three definition styles covered in this chapter: inductive, recursive, and index function.#</li>#
 
-%\item%#<li># Write a dependently-typed interpreter for a simple programming language with ML-style pattern-matching.  The language is defined informally by this grammar:
+%\item%#<li># Write a dependently-typed interpreter for a simple programming language with ML-style pattern-matching, using one of the encodings of heterogeneous lists to represent the different branches of a [case] expression.  (There are other ways to represent the same thing, but the point of this exercise is to practice using those heterogeneous list types.)  The object language is defined informally by this grammar:
 
   [[
 t ::= bool | t + t