@@ -172,3 +172,59 @@ types:
172172\end{SaveVerbatim}
173173\useverb{usetest}
174174
175+\subsection{Parameterised blocks}
176+
177+Groups of functions can be parameterised over a number of arguments using a
178+\texttt{parameters} declaration, for example:
179+
180+\begin{SaveVerbatim}{paramex}
181+
182+parameters (x : Nat, y : Nat)
183+ addAll : Nat -> Nat
184+ addAll z = x + y + z
185+
186+\end{SaveVerbatim}
187+\useverb{paramex}
188+
189+\noindent
190+The effect of a \texttt{parameters} block is to add the declared parameters to every
191+function, type and data constructor within the block. Outside the block, the parameters
192+must be given explicitly:
193+
194+\begin{SaveVerbatim}{addall}
195+
196+*params> :t addAll
197+addAll : Nat -> Nat -> Nat -> Nat
198+
199+\end{SaveVerbatim}
200+\useverb{addall}
201+
202+\noindent
203+Parameters blocks can be nested, and can also include data declarations, in
204+which case the parameters are added explicitly to all type and data
205+constructors. They may also be dependent types with implicit arguments:
206+
207+\begin{SaveVerbatim}{paramdata}
208+
209+parameters (xs : Vect a x, y : Nat)
210+ data Vects : Set -> Set where
211+ MkVects : Vect a y -> Vects a
212+
213+ append : Vects a -> Vect a (x + y)
214+ append (MkVects ys) = xs ++ ys
215+
216+\end{SaveVerbatim}
217+\useverb{paramdata}
218+
219+\noindent
220+To use \texttt{Vects} or \texttt{append} outside the block, we must also
221+give the \texttt{xs} and \texttt{y} arguments. Here, we can use placeholders for
222+the values which can be inferred by the type checker:
223+
224+\begin{SaveVerbatim}{paramuse}
225+
226+*params> show (append _ _ (MkVects [1,2,3] _ [4,5,6]))
227+"[1, 2, 3, 4, 5, 6]" : String
228+
229+\end{SaveVerbatim}
230+\useverb{paramuse}