[Agda] _$_

Serge D. Mechveliani mechvel at botik.ru
Sun Sep 2 11:37:59 CEST 2012

To my

>> For  Agda- + lib-0.6,  
>>      _$_  imported from  Function,  
>> [..]
>> each of the following 4 declarations causes "unsolved metas":
>>   n : Nat
>>   n = suc $ suc 0
>> [..]

Nils Anders Danielsson wrote	

> I suspect that suc is overloaded. Is your code accepted if you write
> ???.suc instead of suc?

Thank you.
           n : Nat
           n = Nat.suc $ Nat.suc 0
does work.
In my module,  suc  is imported from  Data.Nat  and from  Data.Fin.

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:

  suc  is visible at the following locations:

So, I do not fear to write  suc, +,  and such. Because, if an overlapping
import happens, the compiler reports adequately, and it is easy to
understand and to fix -- by adding  `<module-name>.'  or `hiding' or
`using' or `renaming'.

Now, this has bitten me for the first time. Is this a specific of `$' ?



More information about the Agda mailing list