adbe613 · Idris-dev · git.iko.soy

tutorial/interp.tex+1−1

compare with master

unifiedsplit

@@ -344,7 +344,7 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

344$ idris interp.idr

345 ____ __ _

346 / _/___/ /____(_)____

347− / // __ / ___/ / ___/ Version 0.9.2

347+ / // __ / ___/ / ___/ Version 0.9.5

348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

349 /___/\__,_/_/ /_/____/ Type :? for help

350

tutorial/intro.tex+1−1

@@ -62,7 +62,7 @@ verifying systems software.

62\subsection{Example Code}

63

64This tutorial includes some example code, which has been tested with \Idris{} version

65−0.9.2. The files are available in the \Idris{} distribution,

65+0.9.5. The files are available in the \Idris{} distribution,

66so that you can try them out easily,

67under \texttt{tutorial/examples}. However, it is strongly recommended that you

68type them in yourself, rather than simply loading and reading them.

tutorial/modules.tex+56

@@ -172,3 +172,59 @@ types:

172\end{SaveVerbatim}

173\useverb{usetest}

174

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}

tutorial/starting.tex+3−3

@@ -82,7 +82,7 @@ environment. You should see something like the following:

82$ idris

83 ____ __ _

84 / _/___/ /____(_)____

85− / // __ / ___/ / ___/ Version 0.9.2

85+ / // __ / ___/ / ___/ Version 0.9.5

86 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

87 /___/\__,_/_/ /_/____/ Type :? for help

88

@@ -102,7 +102,7 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which

102the program is compiled to the executable \texttt{hello}.

103

104\begin{SaveVerbatim}{cmds}

105−Idris version 0.9.2

105+Idris version 0.9.5

106-------------------

107

108 Command Arguments Purpose

@@ -128,7 +128,7 @@ Idris version 0.9.2

128$ idris hello.idr

129 ____ __ _

130 / _/___/ /____(_)____

131− / // __ / ___/ / ___/ Version 0.9.2

131+ / // __ / ___/ / ___/ Version 0.9.5

132 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

133 /___/\__,_/_/ /_/____/ Type :? for help

134

tutorial/theorems.tex+1−1

@@ -410,7 +410,7 @@ The totality check is currently very conservative. To be recorded as total, a fu

410\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument

411\item Not call any non-total functions

412\item Not use any data types which are not \emph{strictly positive}

413−\item (In version 0.9.2) Not be mutually recursive

413+\item (In version 0.9.5) Not be mutually recursive

414\end{itemize}

415

416\noindent

tutorial/typesfuns.tex+20

@@ -225,6 +225,26 @@ reverse {a} xs = revAcc [] xs where

225\end{SaveVerbatim}

226\useverb{revwhereb}

227

228+\noindent

229+As well as functions, \texttt{where} blocks can include local data

230+declarations, such as the following where \texttt{MyLT} is not accessible outside

231+the definition of \texttt{foo}:

232+

233+\begin{SaveVerbatim}{wheredata}

234+

235+foo : Int -> Int

236+foo x = case isLT of

237+ Yes => x*2

238+ No => x*4

239+ where

240+ data MyLT = Yes | No

241+

242+ isLT : MyLT

243+ isLT = if x < 20 then Yes else No

244+

245+\end{SaveVerbatim}

246+\useverb{wheredata}

247+

228\subsection{Dependent Types}

248\subsection{Dependent Types}

229

249

230\subsubsection{Vectors}

250\subsubsection{Vectors}