RE: Spad and inductive types

"Bill Page" <[email protected]>
Newsgroups gmane.comp.mathematics.axiom.user
Message-ID <054e01c79083$4a61fe00$6900a8c0@asus>
Martin,

On May 7, 2007 4:14 AM you wrote:
> 
> Here you go.  But I doubt somehow that Gaby had this in mind, 
> since this is quite usual stuff in Axiom (grep "Rep.*Union")
> 
> ...

Fantastic! Thankyou. See it again here:

http://wiki.axiom-developer.org/SandBoxInductiveType

I believe that is exactly what Gaby wanted. Yes, grep shows
some examples but not of the specific type of induction that
Gaby had in mind.

It seems that one key differences between what I wrote and
your version was:

...
Rep := Union(MkInt, MkAdd, MkMul)
...

The grep command actually shows one case where ==> is used, but
I have noticed before that Spad seems to treat this differently
than what I always expect but you seem to write it naturally. :-)

Now I can retire to sleep in peace.

Cheers,
Bill Page
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.