# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1224536524 14400
# Node ID 99be59b9e20d4aff12a7b19a05e1bf1b9f8a300d
# Parent  0bfc755024981cb98004a7f233baeb4160902580
s/itree/htree

diff -r 0bfc75502498 -r 99be59b9e20d src/DataStruct.v
--- a/src/DataStruct.v	Mon Oct 20 14:03:08 2008 -0400
+++ b/src/DataStruct.v	Mon Oct 20 17:02:04 2008 -0400
@@ -829,7 +829,7 @@
 
 %\begin{enumerate}%#<ol>#
 
-%\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 [itree] indexed by trees.  The structure of an [itree] 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 [itree] by path.  Define a function [itmap2] for "mapping over two trees in parallel."  That is, [itmap2] takes in two [itree]s with the same index tree, and it forms a new [itree] with the same index by applying a binary function pointwise.
+%\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.
 
   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>#