[opentheory-users] Multiple definitions in base package

[Joe Leslie-Hurd]

Hi Rob,

The HOLLight.* symbols are "auxiliary" type operators and constants that
are used in proofs but not exported by any theory. So it's not unreasonable
that it is defined multiple times in subtheories of base. However, what is
surprising is that the article compression algorithm implemented in the
opentheory tool does not fold the multiple definitions into a single
definition.

Thanks for the report: I'll look into the problem. This code will need
reworking anyway to process the new article commands.

If the multiple definitions are causing problems then as a workaround you
can pick an arbitrary new name for any symbols in the HOLLight namespace,
because such symbols are guaranteed never to be appear in any exported
theorem.

Cheers,

Joe



On Tue, Mar 18, 2014 at 7:56 AM, Rob Arthan <rda at lemma-one.com> wrote:

> I just installed the latest version of the base package and did:
>
>    opentheory info --article --output base.art base
>
> The resulting article file contains multiple definitions of various
> constants in the HOLLight namespace.
> E.g., HOLLight.NUMSUM.
>
> Regards,
>
> Rob.
>
> _______________________________________________
> 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/20140318/bab2cf34/attachment.html>