You are right, but I would state it more like, the arrows cannot be plain HM arrows if the equations are all true.
Lets assume I was mistaken when I said they are HM arrows, and focus on the implications of the equations. K. On 31 March 2015 at 17:05, Matt Oliveri <[email protected]> wrote: > On Tue, Mar 31, 2015 at 11:44 AM, Keean Schupke <[email protected]> wrote: > > Clarification, so: > > > > 1. (a -> b -> c -> d) U (a b c => d) = (a b c => d) > > > > 2. (a -> b) U (a b c => d) = _|_ > > > > 3. (a -> b) U (a -> b -> c -> d) = (a =>b -> c -> d) > > (x U y) is notation for "unify x with y"? If so, then sorry, but I > think you're mistaken. Those equations cannot all be true if the > arrows are HM arrows. See my previous email. > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
