<div dir="ltr"><div>It would be helpful, but I don't think it's urgent. </div>I have made the HOL4 writer detect when a call to defineConstList could be done via defineConst, and use that instead. </div><div class="gmail_extra"> <div class="gmail_quote">On 30 October 2015 at 14:52, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana, Version 5 of the article standard comprises a non-redundant set of commands (as far as I know), so one way of achieving your goal is to downgrade a version 6 article to version 5 as follows: opentheory info --article -o output5.art --output-version 5 input.art This also converts the version 6 defineTypeOp command into the incompatible version 5 defineTypeOp command, so it's exactly what you asked for. Also, the inverse transformation from version 5 articles to version 6: opentheory info --article -o output6.art --output-version 6 input.art is rather simple-minded and doesn't implement the cool pattern recognition to create version 6 derived commands from the non-redundant set of version 5 commands. To help developers using the article format, I had been thinking of adding recipes to the description of the redundant version 6 commands in the article standard showing how to implement them in terms of the non-redundant commands, but I never got around to it. Do you think that would be helpful? Cheers, Joe <div><div class="h5"> On Thu, Oct 29, 2015 at 4:25 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: > (Also, my simulation of defineConst was totally wrong, but I think you get > the idea. It just needs to use typeOf(t) in more places, and make the > variable twice.) > > On 30 October 2015 at 10:23, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: >> >> Even cooler would be to go in the other direction :) >> (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.) >> >> On 30 October 2015 at 10:08, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: >>> >>> I was originally going to suggesting retiring defineConst, but I have >>> realised that what I'm really asking is about redundant commands. >>> >>> The defineConst command is subsumed by the defineConstList command. >>> >>> 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. >>> >>> Then simulating a defineConst command is as easy as doing >>> >>> defineConstList(assume(mk_eq(varTerm(var n),t)),cons n nil) >>> >>> where mk_eq corresponds to making an equality between two terms, and n >>> and t correspond to the arguments to defineConst. >>> >>> I guess there are already redundant commands in the virtual machine, >>> though (like trans). >>> >>> 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. >> >> > > </div></div>> _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </blockquote></div> </div>