[Agda] Instance search and type variables

Nils Anders Danielsson nad at cse.gu.se
Thu Jan 10 11:43:30 CET 2019


On 09/01/2019 11.21, Pavel Perikov wrote:
> Can anyone explain while declaring inst₂ is prohibited?

See the reference manual:

   https://agda.readthedocs.io/en/latest/language/instance-arguments.html#declaring-instances

-- 
/NAD


More information about the Agda mailing list