### changeset 501:28c2fa8af4eb

Pass through Chapter 9
author Adam Chlipala Tue, 05 Feb 2013 12:38:25 -0500 8303abe4a61f 7d2339cbd39c src/DataStruct.v 1 files changed, 3 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
```--- a/src/DataStruct.v	Mon Feb 04 09:57:06 2013 -0500
+++ b/src/DataStruct.v	Tue Feb 05 12:38:25 2013 -0500
@@ -41,7 +41,7 @@
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).

-  (** An instance of [fin] is essentially a more richly typed copy of a prefix of the natural numbers.  The type [fin n] is isomorphic to [{m : nat | m < n}].  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
+  (** An instance of [fin] is essentially a more richly typed copy of a prefix of the natural numbers.  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].

Now it is easy to pick a [Prop]-free type for a selection function.  As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
[[
@@ -276,7 +276,7 @@
Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
HCons (1, 2) (HCons (true, false) HNil).

-(** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
+(** There are many other useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)

(* end thide *)

@@ -570,7 +570,7 @@
"forall n : nat, filist tree n -> tree"
>>

-  The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually inductive types.  We defined [filist] recursively, so it may not be used for nested recursion.
+  The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually inductive types.  We defined [filist] recursively, so it may not be used in nested inductive definitions.

Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, %\index{reflexive inductive type}%reflexive types.  Instead of merely using [fin] to get elements out of [ilist], we can _define_ [ilist] in terms of [fin].  For the reasons outlined above, it turns out to be easier to work with [ffin] in place of [fin]. *)
```