[Agda] underscore in \neg
Matus Tejiscak
ziman at functor.sk
Sun Aug 25 11:29:45 CEST 2013
The underscore is there so that you can write "¬ f x", as opposed to
"not (f x)".
Matus
Quoting 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?
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: PGP Digital Signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130825/956ad020/attachment.bin
More information about the Agda
mailing list