The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 1 Mar 2005 
roconnor AT theorem.ca
 wrote:

> > gfold :: (forall a. m a -> n a) ->
> >             (forall a. n a -> n a -> n a) ->
> >             (forall a. n (Maybe a) -> n a) ->
> >             (forall a. (Maybe (m a)) -> m (Maybe a)) ->
> >             Lambda (m a) -> n B
> > gfold v a l k (Var x) = v x
> > gfold v a l k (App x y) = a (gfold v a l k x) (gfold v a l k y)
> > gfold v a l k (Lambda x) = l (gfold v a l k (lift x))

oops, this last line should instead read

> gfold v a l k (Lambda x) = l (gfold v a l k (lift x k))

where lift :: (Lambda a) -> (a -> b) -> (Lambda b) is the obvious
function.

(Indeed I should be using k somewhere).

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''