<div>Hi Nils,</div><div><br></div><div>Sorry for the delay! I just checked the bug tracker and bug 206 already seems to cover my case.</div><div><br></div><div>I'll try out your suggestion, too.</div><div><br></div><div>
Thanks,</div><div>Dan</div><br><div class="gmail_quote">On Tue, Dec 22, 2009 at 5:40 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cs.nott.ac.uk">nad@cs.nott.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On 2009-12-20 02:26, Daniel Peebles wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This fails with:<br>
<br>
Dec (i' ≡ j) !=< Level of type Set<br>
<br>
on the i ≟ j line, supposedly in the `w' expression. I'm not really<br>
sure where `w' came from so I'm assuming it's from the desugaring of<br>
the with construct.<br>
</blockquote>
<br></div>
Right. It seems as if the auxiliary function generated by the with<br>
machinery does not type check. This looks like a bug. Can you open a<br>
ticket for it?<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
As a workaround, if I manually make a q function that takes the Dec<br>
result of i ≟ j and matches on it, the whole thing works fine.<br>
</blockquote>
<br></div>
An easier option is perhaps to bind E in the top-level definition, so<br>
you don't need to quantify over it in p.<br>
<br>
--<br><font color="#888888">
/NAD<br>
<br>
<br>
</font></blockquote></div><br>