[Agda] Non-termination change in Agda 2.3.3

[Ulf Norell]

That's not using 'with' so it's certainly an unrelated issue.

/ Ulf


On Wed, Mar 26, 2014 at 9:13 AM, Nicolas Pouillard
<np at nicolaspouillard.fr>wrote:

> Quoting Ulf Norell (2014-03-26 07:19:19)
> > This is a consequence of the new termination checking of with functions
> [1].
> > The problem in this case is that the termination checker doesn't see the
> > relationship
> > between as and bs. I don't think this is a big problem though, since it's
> > only an
> > issue if you with-abstract over variables (or constructor patterns),
> which
> > it doesn't
> > make much sense to do.
>
> What about recursive calls in anonymous function definitions (e.g. λ { pat
> ... }),
> I realized a regression where I had to change such a definition on _⊎_
> into an
> eliminator.
>
> Can this be related?
>
> The code:
>
> https://github.com/crypto-agda/protocols/blob/master/Control/Protocol/Multiplicative.agda#L74
>
> Cheers,
> -- NP
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140326/bdd38932/attachment.html