ae1cf53 · Idris-dev · git.iko.soy

CHANGELOG+4−5

compare with master

unifiedsplit

@@ -3,14 +3,13 @@ New in 0.9.1:

3

4User visible changes:

5

6−* DSL notation

6+* DSL notation, for overloading lambda and let bindings

7−* Record projection and update

7+* Dependent records, with projection and update

8* Totality checking and 'total' keyword

9* Auto implicits and default argument values {auto n : T}, {default val n : T}

10−* Additions to prelude, including Nat and List theorems

11* Overlapping type class instances disallowed

10* Overlapping type class instances disallowed

12−* Many extensions to nat and list libraries (mostly thanks to Dominic

11+* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to

13− Mulligan)

12+ Dominic Mulligan)

14* New libraries: control.monad.identity, control.monad.state

13* New libraries: control.monad.identity, control.monad.state

15* Small improvements in error reporting

14* Small improvements in error reporting

16

15

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/provisional.tex+2−4

@@ -24,10 +24,9 @@ We'd like to implement this as follows:

24parity : (n:Nat) -> Parity n

25parity O = even {n=O}

26parity (S O) = odd {n=O}

27−parity (S (S k)) with parity k {

27+parity (S (S k)) with (parity k)

28 parity (S (S (j + j))) | even = even {n=S j}

29 parity (S (S (S (j + j)))) | odd = odd {n=S j}

30−}

31

30

32\end{SaveVerbatim}

31\end{SaveVerbatim}

33\useverb{parfail}

32\useverb{parfail}

@@ -80,10 +79,9 @@ except that they introduce the right hand side with a \texttt{?=} rathar than

80parity : (n:Nat) -> Parity n

79parity : (n:Nat) -> Parity n

81parity O = even {n=O}

80parity O = even {n=O}

82parity (S O) = odd {n=O}

81parity (S O) = odd {n=O}

83−parity (S (S k)) with parity k {

82+parity (S (S k)) with (parity k)

84 parity (S (S (j + j))) | even ?= even {n=S j}

83 parity (S (S (j + j))) | even ?= even {n=S j}

85 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

84 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

86−}

87

85

88\end{SaveVerbatim}

86\end{SaveVerbatim}

89\useverb{paritypro}

87\useverb{paritypro}

tutorial/starting.tex+1−1

@@ -22,7 +22,7 @@ The easiest way to install \Idris{}, if you have all of the prerequisites, is to

22

23\begin{SaveVerbatim}{install}

24

25−cabal install idris

25+cabal update; cabal install idris

26

27\end{SaveVerbatim}

28\useverb{install}

tutorial/theorems.tex+1−1

@@ -345,7 +345,7 @@ from which we could prove anything:

345

346\begin{SaveVerbatim}{empties}

347

348−-- making use of 'head' being partially defined

348+-- making use of 'hd' being partially defined

349empty1 : _|_

350empty1 = hd [] where

351 hd : List a -> a

tutorial/typesfuns.tex+3−3

@@ -557,7 +557,7 @@ greet = do putStr "What is your name? "

557\useverb{greet}

558

559\noindent

560−The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type

560+The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type

561\texttt{IO a}, and

562puts the result, of type \texttt{a} into the variable \texttt{x}.

563In this case, \texttt{getLine} returns an \texttt{IO String},

@@ -608,7 +608,7 @@ names \texttt{Nil} and \texttt{::} can be written in list form. For example:

608

609\begin{itemize}

610\item \texttt{[]} means \texttt{Nil}

611−\item \texttt{[1,2,3]} means \texttt{Cons 1 (Cons 2 (Cons 3 Nil))}

611+\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}

612\end{itemize}

613

614\noindent

@@ -849,7 +849,7 @@ filter p Nil = (_ , [])

849In the \texttt{::} case, we need to inspect the result of a recursive call to

850\texttt{filter} to

851extract the length and the vector from the result. To do this, we use \texttt{with}

852−notation. with allows pattern matching on intermediate values:

852+notation, which allows pattern matching on intermediate values:

853

854\begin{SaveVerbatim}{vfiltercons}

855