[opentheory-users] redundant commands

[Ramana Kumar]

(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 <ramana at member.fsf.org> 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 <ramana at member.fsf.org> 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.
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151030/ceac57ab/attachment.html>