[Agda] Not Unfolding Local Defs

[Harley D. Eades III]

Hi, Andrés.

Thanks for the help!

Unfortunately, prefixing the type and context command with C-u doesn't do
the trick.
It still unfolds those definitions.  So for example, if I run C-u C-l-, I
get the same
type in the hole as C-l-,.

Thanks,
Harley


On Tue, May 10, 2016 at 2:21 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160510/72dbd24f/attachment.html