<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">&lt;<a href="mailto:andres.sicard.ramirez@gmail.com" target="_blank">andres.sicard.ramirez@gmail.com</a>&gt;</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 &lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt; wrote:<br>

&gt;<br>
&gt; P.S.: Agda 1 had a notation<br>
&gt;<br>
&gt;   suc@Nat<br>
&gt;<br>
&gt; for manual constructor disambiguation.  Not a bad idea, maybe we should<br>
&gt; restore it.<br>
&gt;<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>