[Agda] (Stronger) double negation of law of excluded middle

[Kirill Elagin]

Just to clarify what I mean, here is a little example:

~~~~~~~
data List (A : Set) : Set where
  Nil : List A
  Cons : A -> List A -> List A

listid : (A : _) -> List A -> List A
listid _ Nil = Nil
listid _ (Cons x xs) = Cons x (listid _ xs)
~~~~~~~~

The first underscore here means “guess the type” and here is an equivalent
declaration:

~~~~
listid : ∀ A -> List A -> List A
~~~~

Two underscores on the left of the definition both mean “I don’t care about
the name” just like in Haskell.
The underscore on the right means “guess the value” and note that it’s
completely orthogonal to the underscores on the left:

~~~~
listid A (Cons x xs) = Cons x (listid _ xs)
~~~~

is also perfectly valid.

On Wed, Oct 15, 2014 at 12:43 PM, Kirill Elagin <kirelagin at gmail.com> wrote:

> As far as I know, `_` can mean at least three different things.
>
> 1. Like in Haskell, “I don’t care about the name”.
> 2. “Guess the value”, and implicit arguments are basically a convenient
> syntax for placing underscores.
> 3. “Guess the type”, and `\forall` is just sugar for this one.
>
> On Wed, Oct 15, 2014 at 11:48 AM, Andrea Vezzosi <sanzhiyan at gmail.com>
> wrote:
>
>> I don't know if it's on the wiki, but _ in Agda's expressions means
>> "what is uniquely determined by the judgemental equality, using only
>> the information from this mutual block".
>>
>> if no such unique solution can be found the _ is going to be left
>> unspecified and the writer needs to give more details.
>> So, like in this thread :)
>>
>>
>> Cheers,
>> Andrea
>>
>> On Tue, Oct 14, 2014 at 10:58 PM, Peter Hancock <hancock at fastmail.fm>
>> wrote:
>> > On 14/10/2014 21:30, Paolo Capriotti wrote:
>> >>
>> >> On Tue, Oct 14, 2014 at 9:28 PM, Dmytro Starosud <d.starosud at gmail.com
>> >
>> >> wrote:
>> >>>
>> >>> Btw, I was trying to look into this, but there is something missing
>> with
>> >>> it:
>> >>>
>> >>> isProp : Set → Set
>> >>> isProp = _
>> >>>
>> >>> PROP = ∃ λ A → isProp A
>> >
>> >
>> > This is a sidetrack.  I'm puzzled about what "_" means in Agda, and
>> often
>> > encounter this puzzle. (I've no (known) problem with "_" in Haskell,
>> which
>> > AFAIK only
>> > occurs in argument position and means "I need no name for this
>> argument",
>> > and
>> > is a very worthwhile flag that the name would be unused.)
>> >
>> > The way I read the above, "_" means "the obvious thing", which in this
>> case
>> > is
>> > surely the identity. So PROP means "inhabited type".  And isProp A is a
>> > roundabout
>> > way of writing A.
>> >
>> > So not not ((A : Set) -> isProp A -> A + not A) should be trivial. It
>> is the
>> > left
>> > injection, smashed down with not not.
>> >
>> > I completely see that  ((A : Set) -> not not ( A + not A)) (which is
>> true --
>> > no ??)
>> > is something different from not not ( (A : Set) -> A + not A ) (which
>> one
>> > can possibly
>> > find a counterexample for using Kripke models for 2nd order logic, or
>> > whatever is the
>> > latest technology.)
>> >
>> > I'm just asking what "_" means in Agda. It's not obvious to me. Can
>> someone
>> > point me
>> > into the Wiki?
>> >
>> > Peter
>> >
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> 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/20141015/2134dc97/attachment-0001.html