[opentheory-users] Scalable LCF-style proof translation

[Ramana Kumar]

On Fri, Jul 26, 2013 at 11:29 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> In OpenTheory it's up to the reader
> to decide how to process definitions: they're not inherently
> generative. The OpenTheory reader implements a purely functional
> logical kernel, so its definitions are generative, but reading an
> article into HOL Light would make definitions that update the global
> symbol table.
>

I meant to talk about generativity of term-formation operations, not
definitions.
For example, in OpenTheory if you use the const command twice on the same
name, and then constTerm with the same type on the two resulting consts,
the two resulting terms will not be alpha equivalent. This effectively
forces you to put the constTerm into the dictionary as soon as you create
it, so you can reuse the same one.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130726/e2c14ec4/attachment.html>