[opentheory-users] definition of "new" constants?

[Joe Leslie-Hurd]

[cc'ing the opentheory mailing list]

Hi Gunter,

> Somewhere it should be specified what the list of
> external type operators, external constants etc.
> of an article file are. (which would have to
> refer to the state of the virtual machine)

I have introduced the concept of external and defined symbols in the
article spec:

http://www.gilith.com/research/opentheory/article.html

See the explanations of constants and type operators, and also the
commands typeOp, const and axiom.

I have also added some verbiage at the bottom of the Virtual Machine
section describing the constraint that there should not be different
symbols with the same name in exported theorems.

Thank you again for your comments: every new person who reads the
standard and gives feedback improves it for everyone.

> By the way, I made a systematic catalog of the
> article file commands:
> http://page.mi.fu-berlin.de/rote/Software/OpenTheory/opentheory-commands.html

This is an excellent document, thank you for creating it. If it is in
a permanent location would you mind me linking to it from the
OpenTheory project page?

> I noted that opentheory seems to have a lot of "built-in"
> prettyprinting, like 0 for "Number.Natural.zero".
> Or is there a mechanism to define such transformations?

There is a certain amount of built-in pretty-printing intended to
support the standard theory library, but there is no mechanism to
extend it further.

Cheers,

Joe