Strange Naming in Model Theory

Stream: mathlib4

[Jin Wei]

Hi! I was reading the Model Theory section in mathlib4 lately and found an unusual naming in ModelTheory.Basic between lines 288-292:

class Structure where
  funMap : ∀ {n}, L.Functions n → (Fin n → M) → M
  RelMap : ∀ {n}, L.Relations n → (Fin n → M) → Prop

I imagine Structure.funMap should be named as Structure.FunMap. Is there a particular reason for this or it is a typo, possible due to the migration of codes from Lean3?

[Junyan Xu]

I think the current names precisely follow the naming conventions:

Props and Types (or Sort) (inductive types, structures, classes) are in UpperCamelCase.
Functions are named the same way as their return values (e.g. a function of type A → B → C is named as though it is a term of type C).
All other terms of Types (basically anything else) are in lowerCamelCase.

[Jin Wei]

Thanks! That makes sense now.