[Agda] sym in Agda 2.5.1

[John Leo]

Our emails crossed--I had found this as well.

Unfortunately I don't recall just which version I was using prior to 2.5.1;
I thought it was the most recent 2.4.x but I may well be wrong, and I'm not
sure how I can reconstruct that information.  Perhaps it doesn't matter
anyway as long as the 2.5.1 behavior is clearly specified.

Thanks very much Andrés and Andrea for your help.  Incidentally Andrea you
may not remember but we met and talked at OPLSS last year--you were very
helpful then as well!

John

On Tue, Feb 16, 2016 at 5:13 AM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> On 16 February 2016 at 08:03, John Leo <leo at halfaya.org> wrote:
> > Thanks for the pointer to C-u C-u; that is indeed useful.
>
> From the CHANGELOG, it was introduced in Agda 2.4.0.1:
>
> * Key bindings for controlling simplification/normalisation:
>
>   Commands like "Goal type and context" (C-c C-,) could previously be
>   invoked in two ways. By default the output was normalised, but if a
>   prefix argument was used (for instance via C-u C-c C-,), then no
>   explicit normalisation was performed. Now there are three options:
>
>   * By default (C-c C-,) the output is simplified.
>
>   * If C-u is used exactly once (C-u C-c C-,), then the result is
>     neither (explicitly) normalised nor simplified.
>
>   * If C-u is used twice (C-u C-u C-c C-,), then the result is
>     normalised.
>
>
> >  It's still
> > curious that 2.5.1 seems to be evaluating one fewer step by default than
> 2.4
> > did;
>
> There are various 2.4.* versions. Which version you are talking about?
>
>
> --
> Andrés
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160216/5ad26f35/attachment.html