[Agda] when to set underscore suffix?

[James Wood]

¬_ can be combined with itself – see, for example, stdlib's 
Axiom.DoubleNegationElimination 
(https://agda.github.io/agda-stdlib/Axiom.DoubleNegationElimination.html), 
where `¬ ¬ P` can be used instead of `¬ (¬ P)`.

I think you'll find in stdlib that prefix operators tend to have 
symbolic, rather than alphabetic, names (e.g, ¬_, +_, -_). This 
convention probably traces back to the fact that in most other 
programming languages, symbols are handled syntactically differently to 
other names, so the reader is more alert that there might be something 
special happening, even in Agda. In particular, in Haskell, symbolic 
names are always infix, while alphanumeric names behave like normal Agda 
names. The only counterexample to this convention I can think of is 
begin_, used as part of equational reasoning syntax, which I guess is 
supposed to look like a keyword with an unusual syntax following.

James

On 23/11/2020 17:02, mechvel at scico.botik.ru wrote:
> People,
> 
> Standard library has the  ¬_  function for negation.
> Probably, the underscore is set for a better parsing when  ¬  is 
> composed with
> something (?).
> But for example,
>          length : List A -> Nat
> 
> is not suffixed with underscore.
> What is the difference?
> When underscore is good in an unary function name?
> 
> Thanks,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=04%7C01%7Cjames.wood.100%40strath.ac.uk%7Ccf58932699e849abba9e08d88fd1963f%7C631e0763153347eba5cd0457bee5944e%7C0%7C1%7C637417477901481695%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=ZqzykW0JEYA4j8fbSPIUqXisRIL46SGR4xWa7paTExI%3D&reserved=0 
>