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.
