[opentheory-users] Question about defineConstList

[Robert White]

Dear Joe,

Thanks. That helps a lot.

Regards,
Robert



Hi Robert,

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,

Joe


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" [1]. 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.
>
>
> [1] By this, I mean, did you used defineConst or anything to do the
> definition for individual constants there or simply getting the list pushed
> as
>
>> > List [Const c1, ..., Const ck]
>
> --
>
> Regards,
> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
>



-- 

Regards,
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...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150521/4442824d/attachment-0001.html>