[Agda] sym in Agda 2.5.1

[John Leo]

Ah, looking in the changelog I see the definition of C-c C-, was changed,
but that is buried back in the 2.4.0 changes.

I could swear I was using 2.4.x before 2.5.1, so does that mean it was
changed after 2.4.0 and then changed back in 2.5.1, or am I just confused
and must have been using 2.3.x before?

I'm personally fine with either as the default as long as both (or all
three) possibilities are still allowed.  Also as noted in the TODO,
simplification should be explained--exactly how far does it evaluate.

John



On Tue, Feb 16, 2016 at 5:07 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160216/e9df4e0b/attachment-0001.html