Coq은 표준 라이브러리 부터 컨벤션이 개판임


이름에 통일성이 없음.

어떤 모듈 이름은 Zminmax, 다른건 ZMaxMin

Classical_sets Classical_Prop 이런 이상하게 pascal snake 섞은 이름

Permutation은 타입은(명제) 파스칼, constructor는 perm_nil, perm_skip, perm_swap, perm_trans 이렇게 스네이크 쓰는데

option은 타입 이름이 소문자고 constructor는 파스칼 (None, Some)

list는 타입이 소문자, constructor도 소문자(nil, cons)

비슷한 함수의 여러가지 버전이 있을 때 foo1, foo2 쓰는것도 있고 foo_1 foo_2 쓰는것도 있음
첫번째는 1이 안붙고 두번째부터 2가 붙는것도 흔하고, 어떤건 숫자 대신 prime(')이 붙음


표준 라이브러리가 통일된 컨벤션을 제공해주지 못하다 보니 다른 라이브러리들도 제각각일 수 밖에 없음.

진짜 컨벤션 만으로 코딩 의욕이 떨어지는 수준