search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
452 stars 138 forks source link

Make variables names _∙∙_∙∙_ consistent with those in doubleComp-faces and remove an unnecessary space #1029

Closed ShreckYe closed 1 year ago

ShreckYe commented 1 year ago

Hi Maintainers, I am new to Cubical Agda. The variable name order of "x", "y", "z", and "w" is different in the functions _∙∙_∙∙_ and doubleComp-faces which the former depends on, thus "p" and "r" in 2 functions have different types in reading. This confuses beginners like me when I learn their implementations for the first time. I also notice that throughout the library the order of such plain letter variables is different in different functions. Maybe a rule/guideline of a canonical order can be enforced to reduce these confusions. Or ignore me if it's just a trivial beginner problem.

MatthiasHu commented 1 year ago

Thanks! Merging.

MatthiasHu commented 1 year ago

I also notice that throughout the library the order of such plain letter variables is different in different functions. Maybe a rule/guideline of a canonical order can be enforced to reduce these confusions.

There is indeed a lot of inconsistency (in style, naming, ...) in the library. I personally can't imagine a reasonable guideline to decide between "x y z w" and "w x y z". But if you find something that confuses or annoys you and you can fix it quickly, then I do think it is nice to make a PR out of it.