[opentheory-users] Question about the OpenTheory Repo

[Robert White]

Dear Joe,

Thanks very much for the reply.

It looks interesting that we can also play with it in Haskell but I'm not
good at Haskell yet.

Thanks again!
Regards
Robert



On 19 May 2015 at 19:09, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> This is something I've been working on recently - it means that there
> are definitions in the theory package that can be exported as a
> Haskell package. For example, the definitions in base are exported to
> the "opentheory" package on Hackage:
>
> http://hackage.haskell.org/package/opentheory
>
> In general, the Haskell package name is simply the theory name with
> "opentheory-" prepended, unless there is an explicit haskell-name
> declaration in the theory file that overrides this.
>
> You can find some (mostly outdated) information on a previous version
> of this Haskell export in the "Maintaining Verified Software" paper
> and talk at the bottom of
>
> http://www.gilith.com/research/opentheory/
>
> Cheers,
>
> Joe
>
> On Tue, May 19, 2015 at 5:54 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > Dear OpenTheory users and developers,
> >
> > Hello.
> > I wonder if there is any reason there is a "Haskell" part in the base?
> And
> > what does that mean exactly?
> >
> > Thanks!
> >
> > --
> >
> > Regards,
> > Robert White (Shuai Wang)
> > INRIA Deducteam
>



-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150519/b1a66fbe/attachment.html>