d03a437 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix typos in docs

commitd03a43706d2bb83a0d98be3d6e6b03684f5f460a authorMario Lang <mlang@delysid.org> dateThu 21 Dec 2017, 01:31 (9 years ago) parent76e45a3

2 files changed+3−3

compare with master

unifiedsplit

docs/reference/ide-protocol.rst+1−1 docs/reference/syntax-guide.rst+2−2

docs/reference/ide-protocol.rst+1−1

@@ -113,7 +113,7 @@ The available commands include:

113113 Return a highlighted string consisting of the results of making all arguments in serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string) follow their usual implicitness setting.

114114

115115 ``(:elaborate-term TM)``

116− Return a highlighted string consisting of the the core language term corresponding to serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string).

116+ Return a highlighted string consisting of the core language term corresponding to serialised term ``TM`` (which would previously have been sent as the ``tt-term`` property of a string).

117117

118118 ``(:print-definition NAME)``

119119 Return the definition of ``NAME`` as a highlighted string.

docs/reference/syntax-guide.rst+2−2

@@ -168,7 +168,7 @@ The signature of type constructors may use dependent types

168168Records

169169~~~~~~~

170170

171−There is a special syntax for data types with one constructors and

171+There is a special syntax for data types with one constructor and

172172multiple fields.

173173

174174.. code:: idris

@@ -219,7 +219,7 @@ This is syntactic sugar for the following, which is usually preferred:

219219 data Stream : Type -> Type where

220220 (::) a -> Inf (Stream a) -> Stream a

221221

222−Every occurence of the the defined type in a constructor argument will be

222+Every occurence of the defined type in a constructor argument will be

223223wrapped in the ``Inf`` type constructor. This has the effect of delaying the

224224evaluation of the second argument when the data constructor is applied.

225225An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert