[opentheory-users] redundant commands

[Ramana Kumar]

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/bd35c7d1/attachment.html>