[Axiom-developer] Re: conditionally defined functions

[Ralf HEMMECKE]

Hi Martin,

> Suppose you have a category A, taking as parameter a domain P and providing an
> operation f: % -> P. Furthermore, you have a category (or a domain, a package)
> B, taking as parameter a domain Q. Now you want to achieve the following:
>
> If Q is a domain in A, provide a function g: % -> P, using f.

Let me translate this into some code...

define A(P: Cat1): Category == with {
  f: % -> P;
}

-- Assume B should be a domain.
B(Q: Cat2): Cat3 with {
  if Q has A(???) then {g: % -> ???}
}

To me it seems that in order to state that "Q is a domain in A" one 
would have to know the parameter of A. Note that A is a function 
returning a category. The ??? should be something of type Cat1. And I 
don't see this information somewhere available inside the definition of B.

I guess that is not your point. Can you be more precise here?

Ralf