[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