<div dir="ltr"><div>That's not using 'with' so it'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"><<a href="mailto:np@nicolaspouillard.fr" target="_blank">np@nicolaspouillard.fr</a>></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="">> This is a consequence of the new termination checking of with functions [1].<br>
> The problem in this case is that the termination checker doesn't see the<br>
> relationship<br>
> between as and bs. I don't think this is a big problem though, since it's<br>
> only an<br>
> issue if you with-abstract over variables (or constructor patterns), which<br>
> it doesn't<br>
> 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>