On 2012-08-27 18:13, Serge D. Mechveliani wrote: > Agda has taken much of syntax from the Haskell language, > and I like this. > But why does not it take the `case' construct? There is a case function in the standard library: http://www.cse.chalmers.se/~nad/listings/lib-0.6/README.Case.html -- /NAD