<div dir="ltr">Thanks for that. Unfortunately, even with those modifications (updated <a href="http://lpaste.net/143728">here</a>), it's still not quite right. The first error is:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">Pivotal.lagda:213,5: Parse error<br>constructor<ERROR><br> it -- no fields!<br>\end{code}<br>...<br></blockquote></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br><div class="gmail_quote">On Thu, Oct 22, 2015 at 8:07 PM, effectfully <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">See here <a href="https://lists.chalmers.se/pipermail/agda-dev/2015-January/000048.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/pipermail/agda-dev/2015-January/000048.html</a><br>
<span class=""><br>
2015-10-23 5:38 GMT+03:00, Martin Stone Davis <<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>>:<br>
> Would someone help me get Conor's McBride's code to typecheck? I'm trying<br>
> to follow "How to keep your Neighbours in Order", but, unfortunately, the<br>
> following definition does not work in Agda <a href="http://2.4.2.4" rel="noreferrer" target="_blank">2.4.2.4</a>:<br>
><br>
> _:-_ : forall {P T} -> <P P P> -> (P => T) -> T<br>
>> ! :- t = t<br>
>><br>
><br>
> The error is:<br>
><br>
> Instance search can only be used to find elements in a named type<br>
>> when checking that the expression t has type .T<br>
>><br>
><br>
> The complete source can be found in<br>
> <a href="https://github.com/pigworker/Pivotal/blob/master/Pivotal.lagda" rel="noreferrer" target="_blank">https://github.com/pigworker/Pivotal/blob/master/Pivotal.lagda</a>; the<br>
> particular definition at line 266. In case it helps, I've made a copy here<br>
</span>> <<a href="http://lpaste.net/143668" rel="noreferrer" target="_blank">http://lpaste.net/143668</a>>.<br>
<span class="">> --<br>
> Martin Stone Davis<br>
> ps<br>
> Postal/Residential:<br>
> 1223 Ferry St<br>
> Apt 5<br>
> Eugene, OR 97401<br>
</span>> Talk / Text / Voicemail: <a href="tel:%28310%29%20699-3578" value="+13106993578">(310) 699-3578</a> <<a href="tel:3106993578" value="+13106993578">3106993578</a>><br>
<div class="HOEnZb"><div class="h5">> Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a><br>
> Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
><br>
</div></div></blockquote></div><br></div>