On Saturday, 12 September 2015 at 15:13:27 UTC, Robert wrote:
Hi all,
I came across this example, and wondered what your thoughts on
it are:
<snip>
It seems a little unusual to me.
Robert
For what it's worth, I was investigating this initially as a
discussion about adding type-level values in Rust, and how to
handle unusual cases like this. In the process we've managed to
break the Idris type system:
https://github.com/idris-lang/Idris-dev/issues/2609. There's been
quite a lot of interesting discussion about it on the IRC
channels for all three languages :) I'd be interested to know how
other languages handle this, if anyone knows.
