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

[Kirill Elagin]

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/2c59276a/attachment.html