[Agda] type inference error?

[Andrés Sicard-Ramírez]

On Wed, Jan 9, 2013 at 3:45 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>
> P.S.: Agda 1 had a notation
>
>   suc at Nat
>
> for manual constructor disambiguation.  Not a bad idea, maybe we should
> restore it.
>

I guess we can use _∋_ from the standard library:

lemma : ∀ x → (ℕ ∋ suc x) ≡ suc x
lemma _ = refl

-- 
Andrés