@@ -112,7 +112,7 @@ Types
112112
113113In Idris, types are first class values. So a type declaration is the
114114same as just declaration of a variable whose type is ``Type``. In Idris,
115−variables that denote a type must begin with a capital letter. Example:
115+variables that denote a type need not be capitalised. Example:
116116
117117.. code:: idris
118118
@@ -126,6 +126,9 @@ a more interesting example:
126126 MyListType : Type
127127 MyListType = List Int
128128
129+While capitalising types is not required, the rules for generating implicit
130+arguments mean it is often a good idea.
131+
129132.. _syntax-data-types:
130133
131134Data types