[Agda] sym in Agda 2.5.1

[Andrés Sicard-Ramírez]

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