diff src/Coinductive.v @ 349:de7db21a016c

Fix template
author Adam Chlipala <adam@chlipala.net>
date Tue, 25 Oct 2011 10:56:00 -0400
parents f3154417cd41
children bb1a470c1757
line wrap: on
line diff
--- a/src/Coinductive.v	Tue Oct 25 10:51:31 2011 -0400
+++ b/src/Coinductive.v	Tue Oct 25 10:56:00 2011 -0400
@@ -96,7 +96,7 @@
       ]]
 *)
 
-(* end thide *) 
+(* end thide *)
 
 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks.  However, there are important restrictions that are dual to the restrictions on the use of inductive types.  Fixpoints %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls.  Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls.