Mercurial > cpdt > repo
changeset 349:de7db21a016c
Fix template
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 25 Oct 2011 10:56:00 -0400 |
parents | f3154417cd41 |
children | ad315efc3b6b |
files | src/Coinductive.v |
diffstat | 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.