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.
