[Agda] _$_

[Nils Anders Danielsson]

On 2012-09-01 19:33, Serge D. Mechveliani wrote:
> For  Agda-2.3.0.1 + lib-0.6,
>       _$_  imported from  Function,
>       record IntIdeal (n : Nat) ...    my user type,
>
> each of the following 4 declarations causes "unsolved metas":
>
>    n : Nat
>    n = suc $ suc 0
>
>    foo : (g : Nat) -> IntIdeal $ suc $ suc g -> CommutativeRing _ _
>    foo : (g : Nat) -> IntIdeal $ suc (suc g) -> CommutativeRing _ _
>    foo : (g : Nat) -> IntIdeal (suc $ suc g) -> CommutativeRing _ _
>
> But
>               foo : (g : Nat) -> IntIdeal $ suc g -> CommutativeRing _ _
> is compiled.
> What might this mean?

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

-- 
/NAD