[opentheory-users] Question about defineConstList
joe at gilith.com
Wed May 20 17:01:20 UTC 2015
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 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" . 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 (Shuai Wang)
>> INRIA Deducteam
>> opentheory-users mailing list
>> opentheory-users at gilith.com
> opentheory-users mailing list
> opentheory-users at gilith.com
More information about the opentheory-users