[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

Hi Rob,

The above command takes about 45 seconds to complete on my machine and the
> resulting thm.art is 6Mb in size.
>
>
> This looks like it will be useful when you have sorted out the glitches in
> the package names.
>

Over the weekend I made a new release of the standard theory library

http://opentheory.gilith.com/?pkg=base-1.158

so this command now works as intended to extract the "pure theorem" content.

I have now imported the packages, bool, function, unit, pair, natural and
> option. The process is a bit clunky, but is perfectly workable. The Repo
> website is extremely helpful. So I would say my issues with designing a
> reader are resolved.
>

Excellent, very glad to hear it.

One query: is the case constant in the option package really meant to be
> called Data.case.none.some? That doesn't seem to agree with the web page
> for the package.
>

Case constants are treated specially by the opentheory printer, to support
pretty-printing of case expressions. You can see some example case
expressions in the parser theory:

http://opentheory.gilith.com/opentheory/packages/parser-1.100/parser-1.100.html

It's perhaps ugly, but to avoid the need for symbol tables the OpenTheory
convention is to append the name of the constructors to the case constant,
hence Data.Option.case.none.some. This makes it possible to pretty-print

case.none.some x (\a. y a) z

as

case z of none -> x | some a -> y a

You can see the true name and type of the case constant by hovering over it
in the package document (the same goes for all variables and constants).

Cheers,

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140323/65171f52/attachment.html>