<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">In Agda 2.2.8 qualified constructors was added for these kind of problems.<br><br>lemma : ∀ x → ℕ.suc x ≡ suc x<br>
<div class="im">lemma _ = refl</div><br></div><div class="gmail_quote">/Daniel<br></div><div class="gmail_quote"><br>On Wed, Jan 9, 2013 at 10:16 PM, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:andres.sicard.ramirez@gmail.com" target="_blank">andres.sicard.ramirez@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="im">On Wed, Jan 9, 2013 at 3:45 PM, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> wrote:<br>
><br>
> P.S.: Agda 1 had a notation<br>
><br>
> suc@Nat<br>
><br>
> for manual constructor disambiguation. Not a bad idea, maybe we should<br>
> restore it.<br>
><br>
<br>
</div>I guess we can use _∋_ from the standard library:<br>
<br>
lemma : ∀ x → (ℕ ∋ suc x) ≡ suc x<br>
<div class="im">lemma _ = refl<br>
<br>
--<br>
</div><span class=""><font color="#888888">Andrés<br>
</font></span><div class=""><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>