<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Fri, Jul 26, 2013 at 11:29 PM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">In OpenTheory it's up to the reader<br>
to decide how to process definitions: they're not inherently<br>
generative. The OpenTheory reader implements a purely functional<br>
logical kernel, so its definitions are generative, but reading an<br>
article into HOL Light would make definitions that update the global<br>
symbol table.<br></blockquote><div><br></div><div>I meant to talk about generativity of term-formation operations, not definitions.<br>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.<br>

</div></div></div></div>