Re: Spad and inductive types

Ralf Hemmecke <[email protected]>
Newsgroups gmane.comp.mathematics.axiom.user,gmane.comp.lang.aldor
Message-ID <[email protected]>
>> By the way. Today I have learned how to include an integer
>> into the "left" or "right" part of Union(left: Integer, right: 
>> Integer). There appears only an example in the AUG, but not a formal
>> description.
> 
> Please tell. I missing the example. I think this is quite important.

That should have been an exercise to read my mails carefully. ;-)

http://lists.nongnu.org/archive/html/axiom-mail/2007-05/msg00015.html

My first attempt of the file aaa.as (without extend) contained the lines

     MkAdd(x: %, y: %): % == per [Mkadd == [x, y]];
     MkMul(x: %, y: %): % == per [Mkmul == [x, y]];
-- The following two lines work but I haven't found them documented.
-- For the above version see AUG.pdf p. 145.
--    MkAdd(x: %, y: %): % == per union([x, y], Mkadd);
--    MkMul(x: %, y: %): % == per union([x, y], Mkmul);

I found out about the commented version from a compiler message. The 
compiler complained about having two "union" functions available and 
both took two arguments. So I simply tried that out.

That way is, however, not documented in the AUG. (Which means I was 
unable to find it.)

Ralf
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.