[opentheory-users] reuse lemmas in article format

[Joe Leslie-Hurd]

Hi Francois,

Yes, the dictionary is the mechanism for reusing objects (including
theorems) in an article file.

To address your question about naming theorems, the article format is
intended to be written and read by tools, not humans, so there is no
need for a human-readable name. To bridge the gap an article compiler
must create a mapping from human-readable names to integers
(dictionary keys).

Cheers,

Joe

On Wed, May 17, 2017 at 8:16 AM, François Thiré <franth2 at gmail.com> wrote:
> Hi OpenTheory list,
>
> The only way I see to reuse a theorem in a proof with the article format is
> to save the theorem using the dictionary and then make a reference to it
> with the command "ref". But is it the only solution?
>
> By the way, why there is no way to give a name to a theorem? It would be
> easier to reuse a theorem inside a proof for example by using the name of
> the theorem. By easier, I mean writing a compiler to the article format.
>
> Cheers,
>
> François
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>