[opentheory-users] Question about the OpenTheory Repo

[Joe Leslie-Hurd]

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