Mercurial > cpdt > repo
comparison src/DataStruct.v @ 117:d176595cf46e
Clarify exercise wording
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 14 Oct 2008 15:21:02 -0400 |
| parents | 7163cc09270f |
| children | 99be59b9e20d |
comparison
equal
deleted
inserted
replaced
| 116:7163cc09270f | 117:d176595cf46e |
|---|---|
| 841 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e | 841 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e |
| 842 ]] | 842 ]] |
| 843 | 843 |
| 844 [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. | 844 [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. |
| 845 | 845 |
| 846 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># | 846 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.#</li># |
| 847 | 847 |
| 848 #</ol>#%\end{enumerate}% *) | 848 #</ol>#%\end{enumerate}% *) |