>> Martin wrote:
>>> forall A if A has MyCat then CoercibleTo A
>
> Bill Page wrote:
>> I presume that you mean that one might write this in the context
>> of some domain, say B.
>>
>> Isn't this essentially what one might do in defining a package?
>> E.g.
>>
>> MyCoercePac(A:MyCat,X:CatOf(B)): CoercibleTo(A)
>> == add
>> coerce(x:X):A == ...
>
On Wed, Dec 10, 2008 at 6:41 AM, Ralf Hemmecke wrote:
> You probably meant CatOf(A)...
>
No. I meant 'X:CatOf(B)', i.e. X is a domain that has the same
category as the domain B. Martin's original example did not specify
the domain where the statement:
forall A if A has MyCat then CoercibleTo A
occurs. I just said, let the domain that uses this expression be
called B. Then I want to make a kind of "extension" of B via a
package.
> But why so complicated? Shouldn't
>
> MyCoercePac(A:MyCat,X:MyCat): CoercibleTo(A)
> == add
> coerce(x:X):A == ...
>
> do the thing?
Well,
MyCoercePac(A:MyCat,X:SetCategory): CoercibleTo(A)
== add
coerce(x:X):A == ...
would be almost the same time, but it is no longer specific to B so I
can not depend on using much of the functionality that is exported by
B.
> Where exactly would you need CatOf(A)?
That is the reason why it has to be 'CatOf(B)'
Regards,
Bill Page.
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en
-~----------~----~----~----~------~----~------~--~---
