f7c50cf · Idris-dev · git.iko.soy

CHANGELOG+3−1

compare with master

unifiedsplit

@@ -1,4 +1,4 @@

1−0.1.x to 0.9.0:

1+0.1.x to 0.9:

2

3Complete rewrite. User visible changes:

4

@@ -6,6 +6,8 @@ Complete rewrite. User visible changes:

6* New syntax for pairs/dependent pairs

7* Added type classes

8* Added where clauses

9+* Added case expressions, pattern matching let and lambda

10+* Added monad comprehensions

9* Added cumulativity and universe checking

11* Added cumulativity and universe checking

10* Ad-hoc name overloading

12* Ad-hoc name overloading

11 - Resolved by type or explicit namespace

13 - Resolved by type or explicit namespace

tutorial/classes.tex+11−2

@@ -282,8 +282,8 @@ class Monad m => MonadPlus (m : Set -> Set) where {

282\useverb{monadplus}

283

284\noindent

285−In general, a comprehension takes the form \texttt{[ exp | qual ]} where

285+In general, a comprehension takes the form \texttt{[ exp | qual1, qual2, ..., qualn ]} where

286−\texttt{qual} can be one of:

286+\texttt{quali} can be one of:

287

288\begin{itemize}

289\item A generator \texttt{x <- e}

@@ -314,5 +314,14 @@ do { qual1; qual2; ...; qualn; return exp; }

314\end{SaveVerbatim}

315\useverb{comptrans}

316

317+\noindent

318+Using monad comprehensions, an alternative definition for \texttt{m\_add} would be:

319+

320+\begin{SaveVerbatim}{maddb}

321+

322+m_add : Maybe Int -> Maybe Int -> Maybe Int;

323+m_add x y = [ x' + y' | x' <- x, y' <- y ];

324+\end{SaveVerbatim}

325+\useverb{maddb}

317

326

318

327

tutorial/examples/classes.idr+3

@@ -4,5 +4,8 @@ m_add x y = do { x' <- x; -- Extract value from x

4 return (x' + y'); -- Add them

5 };

6

7+m_add' : Maybe Int -> Maybe Int -> Maybe Int;

8+m_add' x y = [ x' + y' | x' <- x, y' <- y ];

9+

7sortAndShow : (Ord a, Show a) => List a -> String;

10sortAndShow : (Ord a, Show a) => List a -> String;

8sortAndShow xs = show (sort xs);

11sortAndShow xs = show (sort xs);

tutorial/idris-tutorial.pdf

Binary file not shown.