161deaa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2854 from jfdm/sphinx-doc-fixes

Various fixes to the Documentation.

commit161deaaae56b3b72d87fda847101a4739fa4b5df authorEdwin Brady <edwin.brady@gmail.com> dateMon 14 Dec 2015, 10:10 (11 years ago) parent5368429 f4d090c

3 files changed+25−16

compare with master

unifiedsplit

docs/tutorial/interp.rst+9−8 docs/tutorial/modules.rst+12−2 docs/tutorial/typesfuns.rst+4−6

docs/tutorial/interp.rst+9−8

@@ -32,13 +32,14 @@ calculated just like any other value:

3232 interpTy TyBool = Bool

3333 interpTy (TyFun A T) = interpTy A -> interpTy T

3434

35−We’re going to define a representation of our language in such a way

36−that only well-typed programs can be represented. We’ll index the

37−representations of expressions by their type and the types of local

38−variables (the context), which we’ll be using regularly as an implicit

39−argument, so we define everything in a ``using`` block (keep in mind

40−that everything after this point needs to be indented so as to be

41−inside the ``using`` block):

35+We're going to define a representation of our language in such a way

36+that only well-typed programs can be represented. We'll index the

37+representations of expressions by their type, **and** the types of

38+local variables (the context). The context can be represented using

39+the ``Vect`` data type, and as it will be used regularly it will be

40+represented as an implicit argument. To do so we define everything in

41+a ``using`` block (keep in mind that everything after this point needs

42+to be indented so as to be inside the ``using`` block):

4243

4344.. code-block:: idris

4445

@@ -153,7 +154,7 @@ that only the branch which is taken need be evaluated:

153154Writing the Interpreter

154155=======================

155156

156−When we evaluate an ``Expr``, we’ll need to know the values in scope,

157+When we evaluate an ``Expr``, we'll need to know the values in scope,

157158as well as their types. ``Env`` is an environment, indexed over the

158159types in scope. Since an environment is just another form of list,

159160albeit with a strongly specified connection to the vector of local

docs/tutorial/modules.rst+12−2

@@ -212,14 +212,24 @@ using a ``parameters`` declaration, for example:

212212 addAll z = x + y + z

213213

214214The effect of a ``parameters`` block is to add the declared parameters

215−to every function, type and data constructor within the block. Outside

216−the block, the parameters must be given explicitly:

215+to every function, type and data constructor within the

216+block. Specifically, adding the parameters to the front of the

217+argument list. Outside the block, the parameters must be given

218+explicitly. The ``addAll`` function, when called from the REPL, will

219+thus have the following type signature.

217220

218221::

219222

220223 *params> :t addAll

221224 addAll : Nat -> Nat -> Nat -> Nat

222225

226+and the following definition.

227+

228+.. code-block:: idris

229+

230+ addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat

231+ addAll x y z = x + y + z

232+

223233Parameters blocks can be nested, and can also include data declarations,

224234in which case the parameters are added explicitly to all type and data

225235constructors. They may also be dependent types with implicit arguments:

docs/tutorial/typesfuns.rst+4−6

@@ -445,7 +445,7 @@ are not given in applications of ``index``; their values can be

445445inferred from the types of the ``Fin n`` and ``Vect n a``

446446arguments. Any name beginning with a lower case letter which appears

447447as a parameter or index in a

448−type declaration, which is not applied to any arguments, will

448+type declaration, which is not applied to any arguments, will

449449*always* be automatically

450450bound as an implicit argument. Implicit arguments can still be given

451451explicitly in applications, using ``{a=value}`` and ``{n=value}``, for

@@ -1057,11 +1057,9 @@ Intermediate values can be calculated using ``let`` bindings:

10571057

10581058.. code-block:: idris

10591059

1060− data Person = MkPerson String Int

1061−

1062− showPerson : Person -> String

1063− showPerson p = let MkPerson name age = p in

1064− name ++ " is " ++ show age ++ " years old"

1060+ mirror : List a -> List a

1061+ mirror xs = let xs' = reverse xs in

1062+ xs ++ xs'

10651063

10661064We can do simple pattern matching in ``let`` bindings too. For

10671065example, we can extract fields from a record as follows, as well as by