[Agda] How does unification work?

[Erik Palmgren]

Den 2019-09-02 kl. 11:12, skrev Nils Anders Danielsson:
> On 01/09/2019 16.44, Erik Palmgren wrote:
>> My new colleague Anders Mörtberg mentioned that in cubicaltt there is
>> a check for identical terms that can speed up unifications.
>> 
>> Could it possible to implement his trick in standard Agda?
> 
> This trick is implemented in Agda (you can turn it off using
> --no-syntactic-equality). In this case I suppose that the problem is
> that one or more implicit arguments are not syntactically equal.
> 

Thanks. I will look for hidden arguments.

Erik