# HG changeset patch # User Adam Chlipala # Date 1224012062 14400 # Node ID d176595cf46e9495553f4452626d62c45a417cf7 # Parent 7163cc09270fbfe161bd5458452bb8251711010f Clarify exercise wording diff -r 7163cc09270f -r d176595cf46e src/DataStruct.v --- a/src/DataStruct.v Tue Oct 14 15:11:14 2008 -0400 +++ b/src/DataStruct.v Tue Oct 14 15:21:02 2008 -0400 @@ -843,6 +843,6 @@ [x] stands for a variable, and [b] stands for a boolean constant. The production for [case] expressions means that a pattern-match includes zero or more pairs of patterns and expressions, along with a default case. - Your interpreter should be implemented in the style demonstrated in this chapter. That is, your definition of expressions should use dependent types to combine syntax and typing rules, such that the type of an expression tells the types of variables that are in scope. You should implement a simple recursive function translating types [t] to [Set], and your interpreter should produce values in the image of this translation.## + Your interpreter should be implemented in the style demonstrated in this chapter. That is, your definition of expressions should use dependent types and de Bruijn indices to combine syntax and typing rules, such that the type of an expression tells the types of variables that are in scope. You should implement a simple recursive function translating types [t] to [Set], and your interpreter should produce values in the image of this translation.## ##%\end{enumerate}% *)