japesinator / idris-bifunctors Goto Github PK

The verified interfaces (ex-classes) appear to be broken in idris 0.10-git:0cbea4a. Export is also broken by the new system, but that's easy to fix; getting the following error message after fixing it:

$ idris --install bifunctors.ipkg
Entering directory `./src'
./Data/Verified/Bifunctor.idr:7:1:
'public' is deprecated. Use 'public export' instead.
Type checking ./Data/Verified/Bifunctor.idr
./Data/Verified/Bifunctor.idr:10:44:
When checking type of constructor of Data.Verified.Bifunctor.VerifiedBifunctor:
When checking an application of function Data.Bifunctor.bimap:
        Type mismatch between
                p a b (Type of x)
        and
                p b b (Expected type)

        Specifically:
                Type mismatch between
                        a
                and
                        b
./Data/Verified/Bifunctor.idr:16:16:VerifiedBifunctor is not a type class
./Data/Verified/Bifunctor.idr:22:16:VerifiedBifunctor is not a type class

Works fine otherwise (with verified interfaces excluded).

I can't seem to find the license for this code. From http://choosealicense.com/no-license [1]:

You’ll have to check with your own legal counsel regarding your particular project, but generally speaking, the absence of a license means that default copyright laws apply. This means that you retain all rights to your source code and that nobody else may reproduce, distribute, or create derivative works from your work.

Did you intend for this code to be open source? If so, can you upload a license, or point me to it?

Thanks!

[1]: See also: the Berne Convention, the international law: http://zvon.org/law/r/bern.html#intro