Mercurial > cpdt > repo
diff src/DataStruct.v @ 130:464db50b210a
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