[Agda] sym in Agda 2.5.1

[Andrés Sicard-Ramírez]

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