Mercurial > cpdt > repo
comparison src/DataStruct.v @ 129:fd52e2a7ffc3
s/reflexive/index function
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 22 Oct 2008 07:50:47 -0400 |
| parents | 99be59b9e20d |
| children | 464db50b210a |
comparison
equal
deleted
inserted
replaced
| 128:99be59b9e20d | 129:fd52e2a7ffc3 |
|---|---|
| 829 | 829 |
| 830 %\begin{enumerate}%#<ol># | 830 %\begin{enumerate}%#<ol># |
| 831 | 831 |
| 832 %\item%#<li># Define a tree analogue of [hlist]. That is, define a parameterized type of binary trees with data at their leaves, and define a type family [htree] indexed by trees. The structure of an [htree] mirrors its index tree, with the type of each data element (which only occur at leaves) determined by applying a type function to the corresponding element of the index tree. Define a type standing for all possible paths from the root of a tree to leaves and use it to implement a function [tget] for extracting an element of an [htree] by path. Define a function [htmap2] for "mapping over two trees in parallel." That is, [htmap2] takes in two [htree]s with the same index tree, and it forms a new [htree] with the same index by applying a binary function pointwise. | 832 %\item%#<li># Define a tree analogue of [hlist]. That is, define a parameterized type of binary trees with data at their leaves, and define a type family [htree] indexed by trees. The structure of an [htree] mirrors its index tree, with the type of each data element (which only occur at leaves) determined by applying a type function to the corresponding element of the index tree. Define a type standing for all possible paths from the root of a tree to leaves and use it to implement a function [tget] for extracting an element of an [htree] by path. Define a function [htmap2] for "mapping over two trees in parallel." That is, [htmap2] takes in two [htree]s with the same index tree, and it forms a new [htree] with the same index by applying a binary function pointwise. |
| 833 | 833 |
| 834 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># | 834 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># |
| 835 | 835 |
| 836 %\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: | 836 %\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: |
| 837 | 837 |
| 838 [[ | 838 [[ |
| 839 t ::= bool | t + t | 839 t ::= bool | t + t |