<div dir="ltr">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.<div><br></div><div>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?</div><div><br></div><div>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.</div><div><br></div><div>John</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 16, 2016 at 5:07 AM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I would argue that we should switch the default back to fully<br>
normalised: I think it's the best default especially for users less in<br>
the know, so that they might have learnt neither the C-u C-u prefix<br>
nor what to expect from definitional equality.<br>
<div><div class="h5"><br>
<br>
<br>
<br>
<br>
<br>
<br>
On Tue, Feb 16, 2016 at 1:54 PM, Andrés Sicard-Ramírez <<a href="mailto:asr@eafit.edu.co">asr@eafit.edu.co</a>> wrote:<br>
> On 14 February 2016 at 02:03, John Leo <<a href="mailto:leo@halfaya.org">leo@halfaya.org</a>> wrote:<br>
>> I have noticed one "regression" of sorts regarding sym of propositional<br>
>> equality--when goals are shown with C-c C-, sym is represented as<br>
>> "Function.flip" whereas before the flip was done explicitly.<br>
><br>
> In a previous thread Andrea Vezzosi wrote<br>
><br>
> On 13 August 2015 at 18:03, Andrea Vezzosi <<a href="mailto:sanzhiyan@gmail.com">sanzhiyan@gmail.com</a>> wrote:<br>
>> Most commands that show types can be prefixed with C-u C-u to get the<br>
>> fully normalized types.<br>
><br>
> In your case you get the previous fully normalised types using C-u C-u C-c C-,.<br>
><br>
><br>
><br>
><br>
> --<br>
> Andrés<br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>