[Agda] Instance arguments and hole types

[Tillmann Rendel]

Hi,

thanks for the answer.

Nils Anders Danielsson wrote:
> 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
>>
> We don't normalise the goal types in the *All Goals* buffer;
> normalisation can sometimes take a lot of time.

But the ⟦ .Γ ⟧Context part appears to be simplified, so I don't 
understand why the other part cannot get simplified as well.


Also, would it be possible to display

> Meaning.⟦ meaning Set ⟦_⟧Type ⟧ .τ₁

as

> ⟦ .τ₁ ⟧?

   Tillmann