[Agda] Agda for CA

[Nils Anders Danielsson]

On 2012-07-16 17:13, Andreas Abel wrote:
> On 15.07.2012 19:58, Serge D. Mechveliani wrote:

>> 2. Is Adga going to join (multiparametric) type classes?

AFAIK there are no immediate plans to add type classes.

>> 2.1. They say that type classes can be easily modelled in Adga by
>>       dependent records, or/and may be, by implicit arguments.
>> Is this so?
>
> Yes.
>
> Currently, however there is no recursive instance search. E.g. in your
> example, you will have to locally instantiate list equality to Bool.
> See below for an example.

You also have the option to pass around dictionaries manually, if you
prefer this to using instance arguments ({{...}}).

-- 
/NAD