[opentheory-users] Error loading articles

[Ramana Kumar]

I like your original theorem metadata proposal better.

But I suppose one could follow your approach with an extra article that
adds names, if one needs names right now.

It may be right to wait for more field testing, that's up to you. Certainly
if I actually end up hacking up custom encoding/decoding schemes for
metadata, I'll keep the list informed.

On 27 October 2015 at 15:28, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> > It looks like you are encoding theorem names via some (undocumented)
> scheme
> > that wraps the theorem as:
> >
> >   |- (\name_of_thm. name_of_thm) conclusion_of_thm
> >
> > Is this going to become a standard format in which to encode theorem
> names,
> > that other article readers should expect? (I presume not!)
>
> It didn't take you long to reverse engineer my little hack to annotate
> theorems with names! Have no fear, my intention is that this scheme is
> private to the HOL Light/OpenTheory interface, which is why the scheme
> is undocumented, and the corresponding metadata files in the theory
> package suggest that they are to be used by HOL Light only:
>
> hol-light.int  --  Mapping the OpenTheory namespace to HOL Light names
> hol-light.art  --  Mapping the set of theorems to HOL Light names
>
> This fits with the existing scheme whereby some theories can be
> exported as Haskell packages, and there are haskell* metadata files in
> the theory package to help perform this export. Naturally other
> theorem provers are welcome to use the HOL Light files in their own
> interface, or alternatively could contribute metadata files of their
> own to the theory package.
>
> > When we last discussed theorem names,
> > (
> http://www.gilith.com/opentheory/mailing-list/2014-November/000438.html
> > and the ensuing discussion), the plan was to standardise on theorem
> > metadata. Has there been any progress on this front?
>
> Thank you for exhuming the theorem metadata proposal from the archive.
> Even a year later I still like the idea of changing the type of
> exported theorems from
>
> thm set
>
> to
>
> (thm, metadata) finite_map
>
> using a scheme for merging meta-data such as the one I sketched out.
> However, perhaps it is better to see how the current scheme with extra
> metadata files evolves before committing to a standard metadata
> scheme?
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151028/8574b567/attachment.html>