4162113 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4264 from mlang/doctypos

4162113Jason Felice9 years ago

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

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

113 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.

114

115 ``(: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).

117

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

119 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

168Records

169~~~~~~~

170

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

172multiple fields.

173

174.. code:: idris

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

219 data Stream : Type -> Type where

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

221

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

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

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

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