Re: [open-axiom-devel] 8-4 and 8/4

[Gabriel D. R. <gd...@in...>]

On Wed, Jul 16, 2008 at 6:27 PM, Ralf Hemmecke <ra...@he...> wrote:
>>> All I want to say is that here are some hidden coercions taking place so
>>> the returned types are just what the interpreter is able to figure out.
>
>> Yes, this is correct.
>> In the interpreter, everytime you have a result of type Integer, and
>> that integer
>> is a constant that can be coerced into a tighter SubDomain of Integer,
>> that is done.
>> The behaviour is controlled by $useIntegerSubDomain.
>
>> If you like dpeendent types you should like it!
>
> Why do you say that has to do with dependent types?

well, clearly the behaviour of the interpreter is that the type of the result
in this case has to depend on the value of the result, not the type recorded by
the domain of computation.


>
> Ralf
>