@@ -212,14 +212,24 @@ using a ``parameters`` declaration, for example:
212 addAll z = x + y + z
212 addAll z = x + y + z
214The effect of a ``parameters`` block is to add the declared parameters
214The effect of a ``parameters`` block is to add the declared parameters
215−to every function, type and data constructor within the block. Outside
215+to every function, type and data constructor within the
216+block. Specifically, adding the parameters to the front of the
216−the block, the parameters must be given explicitly:
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.
220 *params> :t addAll
223 *params> :t addAll
221 addAll : Nat -> Nat -> Nat -> Nat
224 addAll : Nat -> Nat -> Nat -> Nat
226+and the following definition.
228+.. code-block:: idris
230+ addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
231+ addAll x y z = x + y + z
223Parameters blocks can be nested, and can also include data declarations,
233Parameters blocks can be nested, and can also include data declarations,
224in which case the parameters are added explicitly to all type and data
234in which case the parameters are added explicitly to all type and data
225constructors. They may also be dependent types with implicit arguments:
235constructors. They may also be dependent types with implicit arguments: