Style for lower/upper case for initial letter in denotations

[mechvel]

Let Prime, Prime' : Pred ℕ _.
Then
(1) prime-2 : Prime 2
starts with the lower case letter, because is is a function.
Further,
(2) prime⇒Prime' : Prime ⇒ Prime'
has to start with a lower case letter, because it is a function.

(3) ¬Prime[0] : ¬ Prime 0
starts with a lower case letter, because it is a function,
and the second letter is preserved in the upper case, because it is of the type name.

These are my suggestions for the style.
In some places in lib-2.1-rc1 the rules (2) and (3) are satisfied, and in some other places they are broken.

I suggest the rules (1), (2), (3),
have a large code that follows these rules, while lib-2* looks neutral relatively to (2), (3).
Can the team take this style for future?

[MatthewDaggitt]

(1) prime-2 : Prime 2 starts with the lower case letter, because is is a function.

Why is Prime 2 a function?

[mechvel]

I meant that prime-2 is a function, and Prime 2 is its type.

[MatthewDaggitt]

I agree with 1 and 3. As for 2, implications between predicates are usually capitalised.

Please could you provide a list of places where you think we don't follow suggestions 1 and 3.

[mechvel]

For example , consider

record GCD a b ... where ...     -- a version of Nat..GCD

GCD[a,b]→GCD[b,a]  :   (a b  : Carrier )  → GCD a b  → GCD b a

This is not implication between predicates.
a) Needs this function to be called gCD[a,b]→GCD[b,a] ?
b) Needs the first occurrence of → to be replaced with ⇒ ?

[mechvel]

Please could you provide a list of places where you think we don't follow suggestions 1 and 3.

I am not ready to search for this. Here are several places concerning, probably (2):

Data.Nat.Base.agda

n>1⇒nonTrivial : needs nonTrivial be capitalised here?

nonTrivial⇒nonZero : what letters need to be capitalised here?

nonTrivial⇒n>1 : is it all right?

Data/List/Properties.agda

The following function names occur in the source.

selfInverse⇒involutive, selfInverse⇒injective

Data/List//Membership/Setoid/Properties.agda

unique⇒irrelevant : ...	  -- ?

Generally, I do not ask changing the function names contained in lib-2.0.
I ask about naming style in the future Standard library and in applications.

[MatthewDaggitt]

GCD[a,b]→GCD[b,a] : (a b : Carrier ) → GCD a b → GCD b a

There is no such function in the library...

Thanks for the suggestions. I'm a bit confused about what rule for capitalisation you're actually proposing though. Could you give a concrete rule, and show how you would like the examples above to be changed?

[mechvel]

I suggest to start the function names with a lower-case symbols, including implications between predicates.
For example,
nonTrivial⇒NonZero
(NonZero is capitalized here because it is a name of a type and its name is not set here to start a function name).
coprime[a,b]⇒Coprime[b,a] : ∀ {a b} → Coprime a b→ Coprime b a.
There is no difference of whether such function is in standard library or not.
Imagine that it has to be included there. I suggest this naming style.
Further:
¬Coprime[a,b]⇒¬Coprime[b,a] : ∀ {a b} → ¬ Coprime a b→ ¬ Coprime b a
-- because it starts with a non-letter symbol, which I suggest to treat as a lower-case with this respect.

Does the team agree?
If not, let it declare the style in a sufficient detail.
Because it is desirable for applications to follow the naming style of the standard library.