[Agda] Instance arguments and hole types

[Nils Anders Danielsson]

On 2013-05-13 14:34, Tillmann Rendel wrote:
> The Emacs mode reports the following type for the new hole:
>
>> Bind (Meaning.⟦ meaning Set ⟦_⟧Type ⟧ .τ₁) ⟦ .Γ ⟧Context
>
> This is not optimal. I would prefer what I get with C-c C-t:
>
>> Bind ⟦ .τ₁ ⟧Type ⟦ .Γ ⟧Context
>
> What can I do to have the redex (Meaning.⟦ meaning Set ⟦_⟧Type ⟧ .τ₁) automatically reduced here?

We don't normalise the goal types in the *All Goals* buffer;
normalisation can sometimes take a lot of time. I suggest that you use
C-c C-t.

-- 
/NAD