The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

Hello,

I'm working on formalizing the contents of "Kleisli arrows of outrageous
fortune" (https://github.com/jwiegley/coq-haskell/blob/master/Conor.v), and
while I'm most of the way through, I'm having difficulty attempting to encode
the free monad using a modified W-type.  Following an example of something
Conor posted in Coq-club long ago, I've tried this:

    Inductive Kleene {I} (F : (I → Type) → I → Type) (p : I → Type) (i : I) :=
      | Ret : p i → Kleene F p i
      | Do  : (forall q, F q i) → Kleene F p i.

This is around line 970.

However, I have a strong suspicion this can't be right.  Can anyone help me to
find a better direction?

Thanks,
  John