changeset 349:de7db21a016c

Fix template
author Adam Chlipala Tue, 25 Oct 2011 10:56:00 -0400 f3154417cd41 ad315efc3b6b src/Coinductive.v 1 files changed, 1 insertions(+), 1 deletions(-) [+]
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.