Skip to content
Browse files

Some documentation updates

  • Loading branch information...
1 parent 709e330 commit 5399670dd3c8606c5c176b10401fd7ff304d52af Edwin Brady committed Feb 2, 2012
Showing with 15 additions and 7 deletions.
  1. +7 −1 CHANGELOG
  2. +1 −1 idris.cabal
  3. +7 −5 tutorial/classes.tex
  4. BIN tutorial/idris-tutorial.pdf
View
8 CHANGELOG
@@ -8,11 +8,17 @@ User visible changes:
* Totality checking and 'total' keyword
* Auto implicits and default argument values {auto n : T}, {default val n : T}
* Additions to prelude, including Nat and List theorems
-* New libs: control.monad.identity, control.monad.state
+* Overlapping type class instances disallowed
+* Many extensions to nat and list libraries (mostly thanks to Dominic
+ Mulligan)
+* New libraries: control.monad.identity, control.monad.state
+* Small improvements in error reporting
Internal changes:
* Faster compilation (only compiling names which are used)
+* Better type class resolution
+* Lots of minor bug fixes
0.1.x to 0.9.0:
View
2 idris.cabal
@@ -41,7 +41,7 @@ Cabal-Version: >= 1.6
Build-type: Custom
Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
- tutorial/examples/*.idr
+ lib/control/monad/*.idr tutorial/examples/*.idr
source-repository head
type: git
View
12 tutorial/classes.tex
@@ -53,6 +53,7 @@ \section{Type Classes}
\useverb{shownat}
\noindent
+Only one instance of a class can be given for a type --- instances may not overlap.
Instance declarations can themselves have constraints. For example, to define a
\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}
instance for the element type, because we are going to use it to convert each element
@@ -71,11 +72,12 @@ \section{Type Classes}
\useverb{showvec}
\noindent
-\textbf{Remark: } The type of the auxiliary function \texttt{show'} is important. The type
-variables \texttt{a} and \texttt{n} which are part of the instance declaration for
-\texttt{Show (Vect a n)} are fixed across the entire instance declaration. As a result,
-we do not have to constrain \texttt{a} again. Furthermore, it means that if we use
-\texttt{n} in the type, it refers to the length of the outermost list \texttt{xs}. Therefore,
+\textbf{Remark: } The type of the auxiliary function \texttt{show'} is
+important. The type variables \texttt{a} and \texttt{n} which are part of the
+instance declaration for \texttt{Show (Vect a n)} are fixed across the entire
+instance declaration. As a result, we do not have to constrain \texttt{a}
+again. Furthermore, it means that if we use \texttt{n} in the type, it refers
+to the (fixed) length of the outermost list \texttt{xs}. Therefore,
we use a different name for the length \texttt{n'} in \texttt{show'}.
\subsection{Default Definitions}
View
BIN tutorial/idris-tutorial.pdf
Binary file not shown.

0 comments on commit 5399670

Please sign in to comment.
Something went wrong with that request. Please try again.