[opentheory-users] Question about the OpenTheory Repo

Joe Leslie-Hurd joe at gilith.com
Tue May 19 17:09:01 UTC 2015

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:


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




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

More information about the opentheory-users mailing list