|
From: | Marcus Better |
Subject: | Re: [Axiom-math] Dynamically constructed return types |
Date: | Mon, 10 Jan 2005 13:09:10 +0100 |
User-agent: | Mozilla Thunderbird 0.9 (X11/20041124) |
Stephen, Martin,thanks for your help on this. I realize that I need to formulate my question more precisely, and I am trying to explain to myself what I am really trying to do...
it is more a weakness w.r.t axioms ability express dependent signatures. If we could write things like: SAE ==> SimpleAlgebraicExtension f: (ULS, eq: SUP) -> SAE(K, SUP K, eq)
The situation here is somewhat more difficult since eq is not known to the caller, but calculated inside the function f. So the signature could not be written this way.
Marcus
[Prev in Thread] | Current Thread | [Next in Thread] |