Just writing to report the (ugly) workaround that I found for this.
However, it does seem to be a bug to me.
I was writing the VerifiedMonad and VerifiedFunctor typeclasses (you
-- "Incomplete term" error
However, it did work like this:
class Functor f => VerifiedFunctor (f : Set -> Set) where
-- Need this to avoid "Incomplete term" error
I had the same issue with (>>= return) which was fixed similarly.
On Wed, Aug 8, 2012 at 9:31 AM, Alan Pogrebinschi <alan...@gmail.com> wrote:
> I just started playing with Idris and got an error the I could isolate in this short repl session:
> Idris> fmap (+ 5) (Just 1)
> This works fine in ghci. My original error is in a proper idris module, not in the repl.
> I'm using the latest github code.
> Any hint?
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.