<div dir="ltr">I'm sorry I omitted the imports before. The relevant ones are<div><br></div><div><div><font face="monospace, monospace">open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _*_)</font></div><div><font face="monospace, monospace">open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)</font></div></div><div><br></div><div>This is from agda-stdlib; I was using version 0.11 before and am using the new one referenced to work with 2.5.1 now. I looked at the code for both and nothing seemed to have changed regarding sym.</div><div><br></div><div>Thanks for the pointer to C-u C-u; that is indeed useful. It's still curious that 2.5.1 seems to be evaluating one fewer step by default than 2.4 did; I'm not sure if that is intentional or not.</div><div><br></div><div>John</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 16, 2016 at 4:54 AM, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 14 February 2016 at 02:03, John Leo <<a href="mailto:leo@halfaya.org">leo@halfaya.org</a>> wrote:<br>
</span><span class="">> 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>
</span>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>
<span class="HOEnZb"><font color="#888888"><br>
<br>
<br>
<br>
--<br>
Andrés<br>
</font></span></blockquote></div><br></div>