[Agda] Instance arguments and hole types

[Nils Anders Danielsson]

On 2013-05-13 22:30, Tillmann Rendel wrote:
> Nils Anders Danielsson wrote:
>> 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.

It would be easy to normalise all goal types, but I don't want to do
this all the time. One could perhaps add a user option for it. If you
think this is a good idea, please add a feature request to the bug
tracker.

> Also, would it be possible to display
>
>> Meaning.⟦ meaning Set ⟦_⟧Type ⟧ .τ₁
>
> as
>
>> ⟦ .τ₁ ⟧?

What do you mean?

-- 
/NAD