[Agda] underscore in \neg
Wojciech Jedynak
wjedynak at gmail.com
Sun Aug 25 13:03:27 CEST 2013
Hi Sergei,
the difference is that `not` is a function, while \neg is a prefix operator.
In practice you sometimes may want to negate a big expression, say BIG.
With `not` you have a choice between
not (BIG)
and
not $ BIG, (_$_ is available in the Function module)
while \neg allows also
\neg BIG.
So it's a matter of plain convenience.
Best,
Wojtek
2013/8/25 Sergei Meshveliani <mechvel at botik.ru>:
> (this is on Standard library lib-0.7)
>
> People,
> `not' is declared without underscore (which looks natural),
> and `¬_' is declared with underscore.
> Why not omit this latter underscore?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list