[Agda] sym in Agda 2.5.1

[Andrea Vezzosi]

On Tue, Feb 16, 2016 at 2:27 PM, John Leo <leo at halfaya.org> wrote:
> [...]
> 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!
>

Ah yes I remember, Always glad to help!


> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>