Mercurial > cpdt > repo
diff src/DataStruct.v @ 216:d1464997078d
Switch DepList to inductive, not recursive, types
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 11 Nov 2009 14:28:47 -0500 |
parents | f8bcd33bdd91 |
children | 6601384e7e14 |
line wrap: on
line diff
--- a/src/DataStruct.v Wed Nov 11 14:00:04 2009 -0500 +++ b/src/DataStruct.v Wed Nov 11 14:28:47 2009 -0500 @@ -841,7 +841,7 @@ (** 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]. +(** Some of the type family definitions and associated functions from this chapter are duplicated in the [DepList] module of the book source. Some of their names have been changed to be more sensible in a general context. %\begin{enumerate}%#<ol>#