@@ -112,7 +112,7 @@ Types
113In Idris, types are first class values. So a type declaration is the
113In Idris, types are first class values. So a type declaration is the
114same as just declaration of a variable whose type is ``Type``. In Idris,
114same 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:
117.. code:: idris
117.. code:: idris
@@ -126,6 +126,9 @@ a more interesting example:
126 MyListType : Type
126 MyListType : Type
127 MyListType = List Int
127 MyListType = List Int
129+While capitalising types is not required, the rules for generating implicit
130+arguments mean it is often a good idea.
129.. _syntax-data-types:
132.. _syntax-data-types:
131Data types
134Data types