[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 ⟧ .τ₁
>> ⟦ .τ₁ ⟧?
What do you mean?
More information about the Agda