[Agda] sym in Agda 2.5.1

[Andrea Vezzosi]

I would argue that we should switch the default back to fully
normalised: I think it's the best default especially for users less in
the know, so that they might have learnt neither the C-u C-u prefix
nor what to expect from definitional equality.







On Tue, Feb 16, 2016 at 1:54 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> On 14 February 2016 at 02:03, John Leo <leo at halfaya.org> wrote:
>> I have noticed one "regression" of sorts regarding sym of propositional
>> equality--when goals are shown with C-c C-, sym is represented as
>> "Function.flip" whereas before the flip was done explicitly.
>
> In a previous thread Andrea Vezzosi wrote
>
> On 13 August 2015 at 18:03, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>> Most commands that show types can be prefixed with C-u C-u to get the
>> fully normalized types.
>
> In your case you get the previous fully normalised types using C-u C-u C-c C-,.
>
>
>
>
> --
> Andrés
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda