[Agda] _$_

Nils Anders Danielsson nad at chalmers.se
Sun Sep 2 15:51:58 CEST 2012


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


More information about the Agda mailing list