[Agda] Instance arguments and hole types

Nils Anders Danielsson nad at cse.gu.se
Tue May 14 11:18:36 CEST 2013

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

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

What do you mean?


More information about the Agda mailing list