Mercurial > cpdt > repo

comparison src/Coinductive.v @ 349:de7db21a016c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix template
author Adam Chlipala <adam@chlipala.net>
date Tue, 25 Oct 2011 10:56:00 -0400
parents f3154417cd41
children bb1a470c1757
comparison
equal deleted inserted replaced
348:f3154417cd41 349:de7db21a016c
94 :: true :: false :: true :: false :: true :: false :: nil 94 :: true :: false :: true :: false :: true :: false :: nil
95 : list bool 95 : list bool
96 ]] 96 ]]
97 *) 97 *)
98 98
99 (* end thide *) 99 (* end thide *)
100 100
101 (** 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. 101 (** 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.
102 102
103 The restriction for co-inductive types shows up as the %\index{guardedness condition}\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell. 103 The restriction for co-inductive types shows up as the %\index{guardedness condition}\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell.
104 [[ 104 [[