4162113 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4264 from mlang/doctypos

Fix typos in docs

commit41621137741d85f759664f0b8fb266e1a6f388b4 authorJason Felice <jason.m.felice@gmail.com> dateThu 21 Dec 2017, 08:34 (9 years ago) parent1e4133b d03a437

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