<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 -> List A -> List A<br><br>listid : (A : _) -> List A -> 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 -> List A -> 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"><<a href="mailto:kirelagin@gmail.com" target="_blank">kirelagin@gmail.com</a>></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"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don't know if it's on the wiki, but _ in Agda's expressions means<br>
"what is uniquely determined by the judgemental equality, using only<br>
the information from this mutual block".<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 <<a href="mailto:hancock@fastmail.fm" target="_blank">hancock@fastmail.fm</a>> wrote:<br>
> On 14/10/2014 21:30, Paolo Capriotti wrote:<br>
>><br>
>> On Tue, Oct 14, 2014 at 9:28 PM, Dmytro Starosud <<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>><br>
>> wrote:<br>
>>><br>
>>> Btw, I was trying to look into this, but there is something missing with<br>
>>> it:<br>
>>><br>
>>> isProp : Set → Set<br>
>>> isProp = _<br>
>>><br>
>>> PROP = ∃ λ A → isProp A<br>
><br>
><br>
> This is a sidetrack. I'm puzzled about what "_" means in Agda, and often<br>
> encounter this puzzle. (I've no (known) problem with "_" in Haskell, which<br>
> AFAIK only<br>
> occurs in argument position and means "I need no name for this argument",<br>
> and<br>
> is a very worthwhile flag that the name would be unused.)<br>
><br>
> The way I read the above, "_" means "the obvious thing", which in this case<br>
> is<br>
> surely the identity. So PROP means "inhabited type". And isProp A is a<br>
> roundabout<br>
> way of writing A.<br>
><br>
> So not not ((A : Set) -> isProp A -> A + not A) should be trivial. It is the<br>
> left<br>
> injection, smashed down with not not.<br>
><br>
> I completely see that ((A : Set) -> not not ( A + not A)) (which is true --<br>
> no ??)<br>
> is something different from not not ( (A : Set) -> A + not A ) (which one<br>
> can possibly<br>
> find a counterexample for using Kripke models for 2nd order logic, or<br>
> whatever is the<br>
> latest technology.)<br>
><br>
> I'm just asking what "_" means in Agda. It's not obvious to me. Can someone<br>
> point me<br>
> into the Wiki?<br>
><br>
> Peter<br>
><br>
><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>
_______________________________________________<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>