[Agda] Not Unfolding Local Defs

[Andrés Sicard-Ramírez]

On 10 May 2016 at 12:26, Harley Eades III <harley.eades at gmail.com> wrote:
> Is there a way to tell Agda not to unfold these definitions in goals?

>From http://agda.readthedocs.io/en/latest/tools/emacs-mode.html :

Commands working with types can be prefixed with C-u to compute type
without further normalisation and with C-u C-u to compute normalised
types.

See also https://github.com/agda/agda/issues/1868 .

-- 
Andrés