<div dir="ltr">Just to clarify what I mean, here is a little example:<br><br>~~~~~~~<br>data List (A : Set) : Set where<br>  Nil : List A<br>  Cons : A -&gt; List A -&gt; List A<br><br>listid : (A : _) -&gt; List A -&gt; List A<br>listid _ Nil = Nil<br>listid _ (Cons x xs) = Cons x (listid _ xs)<br>~~~~~~~~<br><br>The first underscore here means “guess the type” and here is an equivalent declaration:<br><br>~~~~<br>listid : ∀ A -&gt; List A -&gt; List A<br>~~~~<br><br>Two underscores on the left of the definition both mean “I don’t care about the name” just like in Haskell.<br>The underscore on the right means “guess the value” and note that it’s completely orthogonal to the underscores on the left:<br><br>~~~~<br>listid A (Cons x xs) = Cons x (listid _ xs)<br>~~~~<br><br>is also perfectly valid.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 15, 2014 at 12:43 PM, Kirill Elagin <span dir="ltr">&lt;<a href="mailto:kirelagin@gmail.com" target="_blank">kirelagin@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">As far as I know, `_` can mean at least three different things.<br><br>1. Like in Haskell, “I don’t care about the name”.<br>2. “Guess the value”, and implicit arguments are basically a convenient syntax for placing underscores.<br>3. “Guess the type”, and `\forall` is just sugar for this one.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 15, 2014 at 11:48 AM, Andrea Vezzosi <span dir="ltr">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don&#39;t know if it&#39;s on the wiki, but _ in Agda&#39;s expressions means<br>
&quot;what is uniquely determined by the judgemental equality, using only<br>
the information from this mutual block&quot;.<br>
<br>
if no such unique solution can be found the _ is going to be left<br>
unspecified and the writer needs to give more details.<br>
So, like in this thread :)<br>
<br>
<br>
Cheers,<br>
Andrea<br>
<div><div><br>
On Tue, Oct 14, 2014 at 10:58 PM, Peter Hancock &lt;<a href="mailto:hancock@fastmail.fm" target="_blank">hancock@fastmail.fm</a>&gt; wrote:<br>
&gt; On 14/10/2014 21:30, Paolo Capriotti wrote:<br>
&gt;&gt;<br>
&gt;&gt; On Tue, Oct 14, 2014 at 9:28 PM, Dmytro Starosud &lt;<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>&gt;<br>
&gt;&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Btw, I was trying to look into this, but there is something missing with<br>
&gt;&gt;&gt; it:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; isProp : Set → Set<br>
&gt;&gt;&gt; isProp = _<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; PROP = ∃ λ A → isProp A<br>
&gt;<br>
&gt;<br>
&gt; This is a sidetrack.  I&#39;m puzzled about what &quot;_&quot; means in Agda, and often<br>
&gt; encounter this puzzle. (I&#39;ve no (known) problem with &quot;_&quot; in Haskell, which<br>
&gt; AFAIK only<br>
&gt; occurs in argument position and means &quot;I need no name for this argument&quot;,<br>
&gt; and<br>
&gt; is a very worthwhile flag that the name would be unused.)<br>
&gt;<br>
&gt; The way I read the above, &quot;_&quot; means &quot;the obvious thing&quot;, which in this case<br>
&gt; is<br>
&gt; surely the identity. So PROP means &quot;inhabited type&quot;.  And isProp A is a<br>
&gt; roundabout<br>
&gt; way of writing A.<br>
&gt;<br>
&gt; So not not ((A : Set) -&gt; isProp A -&gt; A + not A) should be trivial. It is the<br>
&gt; left<br>
&gt; injection, smashed down with not not.<br>
&gt;<br>
&gt; I completely see that  ((A : Set) -&gt; not not ( A + not A)) (which is true --<br>
&gt; no ??)<br>
&gt; is something different from not not ( (A : Set) -&gt; A + not A ) (which one<br>
&gt; can possibly<br>
&gt; find a counterexample for using Kripke models for 2nd order logic, or<br>
&gt; whatever is the<br>
&gt; latest technology.)<br>
&gt;<br>
&gt; I&#39;m just asking what &quot;_&quot; means in Agda. It&#39;s not obvious to me. Can someone<br>
&gt; point me<br>
&gt; into the Wiki?<br>
&gt;<br>
&gt; Peter<br>
&gt;<br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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></div></blockquote></div><br></div>