<div dir="ltr">Thanks for that. Unfortunately, even with those modifications (updated <a href="http://lpaste.net/143728">here</a>), it&#39;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&lt;ERROR&gt;<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">&lt;<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>&gt;</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 &lt;<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>&gt;:<br>
&gt; Would someone help me get Conor&#39;s McBride&#39;s code to typecheck? I&#39;m trying<br>
&gt; to follow &quot;How to keep your Neighbours in Order&quot;, but, unfortunately, the<br>
&gt; following definition does not work in Agda <a href="http://2.4.2.4" rel="noreferrer" target="_blank">2.4.2.4</a>:<br>
&gt;<br>
&gt; _:-_ : forall {P T} -&gt; &lt;P P P&gt; -&gt; (P =&gt; T) -&gt; T<br>
&gt;&gt; ! :- t = t<br>
&gt;&gt;<br>
&gt;<br>
&gt; The error is:<br>
&gt;<br>
&gt; Instance search can only be used to find elements in a named type<br>
&gt;&gt; when checking that the expression t has type .T<br>
&gt;&gt;<br>
&gt;<br>
&gt; The complete source can be found in<br>
&gt; <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>
&gt; particular definition at line 266. In case it helps, I&#39;ve made a copy here<br>
</span>&gt; &lt;<a href="http://lpaste.net/143668" rel="noreferrer" target="_blank">http://lpaste.net/143668</a>&gt;.<br>
<span class="">&gt; --<br>
&gt; Martin Stone Davis<br>
&gt; ps<br>
&gt; Postal/Residential:<br>
&gt; 1223 Ferry St<br>
&gt; Apt 5<br>
&gt; Eugene, OR 97401<br>
</span>&gt; Talk / Text / Voicemail: <a href="tel:%28310%29%20699-3578" value="+13106993578">(310) 699-3578</a> &lt;<a href="tel:3106993578" value="+13106993578">3106993578</a>&gt;<br>
<div class="HOEnZb"><div class="h5">&gt; Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a><br>
&gt; Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
&gt;<br>
</div></div></blockquote></div><br></div>