[Agda] sym in Agda 2.5.1

[John Leo]

I'm sorry I omitted the imports before.  The relevant ones are

open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _*_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym;
trans; cong)

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.

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.

John

On Tue, Feb 16, 2016 at 4:54 AM, 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160216/d9180d1d/attachment.html