Mercurial > cpdt > repo

diff src/DataStruct.v @ 130:464db50b210a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Clarify intent to use hlist
author Adam Chlipala <adamc@hcoop.net>
date Wed, 22 Oct 2008 09:43:37 -0400
parents fd52e2a7ffc3
children cbf2f74a5130
line wrap: on
line diff
--- 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