Re: M0030 -- Level 1 constructors
Michel, P1788
On 3 Dec 2011, at 17:41, Michel Hack wrote:
>> The operation nums2interval(l,u), where l and u are extended-real
>> values, returns the set {x in R | l <= x <= u}. If (see subclause
>> 5.2) the conditions l <= u , l < +oo and u > -oo hold, this set is
>> the nonempty interval [l,u] and the operation is said to succeed.
>> Otherwise the operation is said to fail, and returns Empty.
>
> Do extended reals exist at level 1? I don't think so -- what does
> exist is unbounded intervals. So at level 1 we need the following
> constructors, where l and u are Reals:
I disagree with the premiss of this. Extended reals do exist at Level 1, in the restricted context of numerical values used to help construct intervals. Or of numerical attributes of intervals, as in the radius, or upper bound, of Entire. The fact that infinity cannot be a *member* of an interval is beside the point.
So I'm perfectly relaxed with my text as it is.
Would you argue "characters don't exist at Level 1, therefore one cannot use a text string as argument to a constructor"? The two cases are essentially equivalent.
John