convention: types and type constructors capitalized?

[Profpatsch]

I was wondering (while trying to understand the code) whether it would make sense to have a convention that types and type constructors (intuitively all files that end in -> ∀ …) are given (file) names starting with a capital letter?

e.g. I wondered what the difference between /recursive and /Mu/recursive was, until I saw that inside the latter the former is imported in a type annotation. I’d rename the former to /Recursive instead, to make them easier to distinguish. Same with all other files that evaluate to types.

[sellout]

Yeah, I absolutely agree. 👍🏼

[sellout]

I think this has happened everywhere now.