<div dir="ltr"><div>That&#39;s not using &#39;with&#39; so it&#39;s certainly an unrelated issue.<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Mar 26, 2014 at 9:13 AM, Nicolas Pouillard <span dir="ltr">&lt;<a href="mailto:np@nicolaspouillard.fr" target="_blank">np@nicolaspouillard.fr</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Quoting Ulf Norell (2014-03-26 07:19:19)<br>
<div class="">&gt; This is a consequence of the new termination checking of with functions [1].<br>
&gt; The problem in this case is that the termination checker doesn&#39;t see the<br>
&gt; relationship<br>
&gt; between as and bs. I don&#39;t think this is a big problem though, since it&#39;s<br>
&gt; only an<br>
&gt; issue if you with-abstract over variables (or constructor patterns), which<br>
&gt; it doesn&#39;t<br>
&gt; make much sense to do.<br>
<br>
</div>What about recursive calls in anonymous function definitions (e.g. λ { pat ... }),<br>
I realized a regression where I had to change such a definition on _⊎_ into an<br>
eliminator.<br>
<br>
Can this be related?<br>
<br>
The code:<br>
<a href="https://github.com/crypto-agda/protocols/blob/master/Control/Protocol/Multiplicative.agda#L74" target="_blank">https://github.com/crypto-agda/protocols/blob/master/Control/Protocol/Multiplicative.agda#L74</a><br>


<br>
Cheers,<br>
-- NP<br>
</blockquote></div><br></div>