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