Re: [isabelle] Malformed dependency error with overloading
On 05/27/2016 01:18 PM, OndÅej KunÄar wrote:
Therefore we impose an additional restriction that makes the problem
quadratic. I call the restriction composability:
for all d_\tau == ... and
c == ... d_\sigma ...
\sigma must be an instance of \tau or \tau must be an instance of \sigma.
(More can be found in my PhD thesis (chapter 3.5)).
Of course, I missed one case.
\sigma must be an instance of \tau or \tau must be an instance of \sigma
*or they are not unifiable*.
That said, composability wants to rule out the case that the two types
have a non-trivial common instance.
This archive was generated by a fusion of
Pipermail (Mailman edition) and