<div dir="ltr"><div>Even cooler would be to go in the other direction :)<br></div>(I mean see an article snippet that looks like it's doing defineConst or trans or something, in terms of more primitive commands, and turn it into a call to the derived command instead.)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 30 October 2015 at 10:08, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div><div>I was originally going to suggesting retiring defineConst, but I have realised that what I'm really asking is about redundant commands.<br></div><div><br>The defineConst command is subsumed by the defineConstList command.<br></div><div><br></div><div>Unfortunately, I can't write an implementation of defineConst purely in terms of other article commands, because the virtual machine provides no mechanism for retrieving the type of a term, or for keeping track of available keys in the dictionary. However, any article writer will be able to do these things.<br><br></div><div>Then simulating a defineConst command is as easy as doing<br><br>defineConstList(assume(mk_eq(varTerm(var n),t)),cons n nil)<br><br></div><div>where mk_eq corresponds to making an equality between two terms, and n and t correspond to the arguments to defineConst.<br><br></div><div>I guess there are already redundant commands in the virtual machine, though (like trans). <br><br>I guess it would be nice (to readers) if there were some switches in the opentheory tool to produce an article with certain redundant commands expanded out into a minimal non-redundant core set of commands.<br></div></div></div></div></div></div></div></div></div>
</blockquote></div><br></div>