[opentheory-users] Question about defineConstList
ai.robert.wangshuai at gmail.com
Thu May 21 11:42:51 UTC 2015
Thanks. That helps a lot.
One thing that may be useful to you when implementing a reader for the
defineConstList command: if you have an article foo.art you are trying
to read, then the command
opentheory info --article --output-version 5 -o bar.art foo.art
will generate a version 5 article file bar.art that is *logically
equivalent* to foo.art. And since defineConstList did not exist in
version 5 of the article format, the same definitions will be made
using only defineConst.
I hope that helps,
On 20 May 2015 at 18:27, Robert White <ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe and other users,
> I wonder if in the defineConstList
> <http://www.gilith.com/research/opentheory/article-5-6.html#defineConstListCommand> ,
> do you actually define the consts first? Or simply use the const "from
> construction" . This function is now causing problems in my code and I
> can't find out where exact the problem is. It would be very nice if you can
> explain a bit more.
> Thanks a lot.
>  By this, I mean, did you used defineConst or anything to do the
> definition for individual constants there or simply getting the list pushed
>> > List [Const c1, ..., Const ck]
> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the opentheory-users