@edwinbrady that does sound slightly terrifying. Guard the definition of such with some proof obligations of sanity?
-
-
-
@cartazio It's hard to know what the proof obligations would be though. My plan is to use this feature exactly once :).
End of conversation
New conversation -
-
-
This Tweet is unavailable.
-
@raichoo@edwinbrady is it some subset of coercive subtyping? - 1 more reply
-
-
-
@edwinbrady Is that necessary if all you're after is syntactic aesthetics? -
@milessabin@raichoo@tailcalled I don't mean the whole lot, just implicit type conversions. Like Coq's "Coercion" syntax. - 5 more replies
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.