proposed @noreturn attribute
Timon Gehr via Digitalmars-d
digitalmars-d at puremagic.com
Wed Jul 19 07:52:28 PDT 2017
On 19.07.2017 16:47, Moritz Maxeiner wrote:
> On Wednesday, 19 July 2017 at 14:32:24 UTC, Timon Gehr wrote:
>> On 19.07.2017 14:13, Moritz Maxeiner wrote:
>>> On Wednesday, 19 July 2017 at 11:35:47 UTC, Timon Gehr wrote:
>>>> a value of type bottom can be used to construct a value for any
>>>> other type.
>>>
>>> AFAIK from type theory, bottom is defined as having no values (so one
>>> can't reason about the relationship of such non-existent value(s) to
>>> values of other types).
>> https://en.wikipedia.org/wiki/Principle_of_explosion
>
> I am aware, but once a statement (and its negation) can be inferred from
> the same (false) proposition, one isn't reasoning anymore - and more
> importantly its not useful w.r.t. explaining what the bottom type is.
I disagree with both of those statements, but I'm not sure how any of
this relates to the true sentence I wrote that you seemed to criticize.
More information about the Digitalmars-d
mailing list