[opentheory-users] Question about defineConstList

[Joe Leslie-Hurd]

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 Wed, May 20, 2015 at 9:31 AM, Ramana Kumar <ramana at member.fsf.org> wrote:
> defineConstList defines the constants, they do not need to be defined before
> that command is executed.
>
> On 20 May 2015 at 17:27, Robert White <ai.robert.wangshuai at gmail.com> wrote:
>>
>> Dear Joe and other users,
>>
>> I wonder if in the defineConstList , 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 (Shuai Wang)
>> INRIA Deducteam
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>