On 2012-09-02 11:37, Serge D. Mechveliani wrote: > But it is strange that Agda reports "unsolved metas" for `suc $ suc 0'. > I have got used that rather it reports of an overlapping import, > like this: Constructors can be overloaded (and nothing else). -- /NAD