[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?


More information about the Agda mailing list