[Agda] type inference error?

[Daniel Gustafsson]

In Agda 2.2.8 qualified constructors was added for these kind of problems.

lemma : ∀ x → ℕ.suc x ≡ suc x
lemma _ = refl

/Daniel

On Wed, Jan 9, 2013 at 10:16 PM, Andrés Sicard-Ramírez <
andres.sicard.ramirez at gmail.com> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130109/20ac0e8f/attachment.html