@edwinbrady Does Idris have or plan to have anything similar to Coercible and type roles, or have you given it any thought?
(I was thinking about the problem of intrinsically typed de Bruijn *levels*, and thought this may be part of the solution... I'm not sure if it would be!)
My first reaction to this sort of question is often "maybe it can already do that" though :)
-
-
Yes it's entirely possible that that's the answer, I only just started playing around with Idris a few days ago. :)
-
(Oh I see https://www.idris-lang.org/docs/current/base_doc/docs/Data.Erased.html … exists. I wonder if that might help...)
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.