[Agda] Re: problem using "with"

Nils Anders Danielsson nad at chalmers.se
Tue May 15 12:03:13 CEST 2012


On 2012-05-15 11:36, Altenkirch Thorsten wrote:
>
> On 15/05/2012 10:24, "Nils Anders Danielsson"<nad at chalmers.se>  wrote:
>
>> AFAIR your approach was restricted to first-order data. Can you handle
>> everything now?
>
> Do you want to pattern match on functions?

Can you handle finite types, Σ, recursive types and equality?

-- 
/NAD



More information about the Agda mailing list