Agda-stdlib: Data.Nat.Properties.≤+≢⇒<

[mechvel]

It looks like ≤,≢⇒< or ≤and≢⇒< have a better mnemonic than ≤+≢⇒<,
because there is no + in its type.

[MatthewDaggitt]

Hmm, you're right the name is a little confusing. I'm not sure about the alternatives though:

• ≤,≢⇒< makes it look like it has a product type in it and the binding order isn't very clear.
• ≤and≢⇒< is very non-standard.
• ≤∧≢⇒< is very difficult to parse as ∧ looks like a flipped inequality.

Thoughts?

[mechvel]

≤→≢→<

[HuStmpHrrr]

I agree with this issue. + looks like a disjunction to be honest. otherwise, ≤×≢⇒< is also an alternative if we want to express conjunction. In this way, we then have way to express disjunction in antecedent by using +.

there are other modules using the same naming convention. probably it can be discussed in larger extent to make sure the naming convention makes better sense.

[MatthewDaggitt]

there are other modules using the same naming convention. probably it can be discussed in larger extent to make sure the naming convention makes better sense.

Do you have others in mind apart from Algebra.FunctionProperties.Consequences?

[HuStmpHrrr]

Data.Fin.Properties also has ≤+≢⇒<. I cannot find any other than this.

Worth mentioning that Relation.Binary.Consequences uses ∧. I find it's better than +.

[MatthewDaggitt]

Hmm I'm also coming round to ∧ as well. It's used liberally elsewhere in the library to stand for and and it isn't overloaded.

≤→≢→< isn't bad either but it's not used anywhere else in the library...