Pattern-matching exercise

src/DataStruct.v

@@ -823,6 +823,8 @@ Qed.
 
 (** * Exercises *)
 
+(** remove printing * *)
+
 (** Some of the type family definitions from this chapter are duplicated in the [DepList] module of the book source.  Only the recursive versions of length-indexed and heterogeneous lists are included, and they are renamed without the [f] prefixes, e.g., [ilist] in place of [filist].
 
 %\begin{enumerate}%#<ol>#
@@ -831,4 +833,16 @@ Qed.
 
   Repeat this process so that you implement each definition for each of the three definition styles covered in this chapter: inductive, recursive, and reflexive.#</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:
+
+  [[
+t ::= bool | t + t
+p ::= x | b | inl p | inr p
+e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e
+]]
+
+  [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.#</li>#
+
 #</ol>#%\end{enumerate}% *)