[opentheory-users] Error loading articles

[Joe Leslie-Hurd]

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