96c9239 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Reference docs: correct sentence about type syntax.

Types don't actually need to be capitalised, unlike Haskell. Someone should write a section on how implicit arguments work, but for now this is at least less wrong.

commit96c92393157ff1ce56fc005a4cf3f958d9afe876 authorEcho Nolan <echo@echonolan.net> dateWed 14 Oct 2015, 17:56 (11 years ago) parent8bd99ed

1 file changed+4−1

compare with master

unifiedsplit

docs/reference/syntax-guide.rst+4−1

docs/reference/syntax-guide.rst+4−1

@@ -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